Convert ident to string in ltac

Using Coq
1

This problem is partly related to coq/7922. In that issue, a hack is proposed to convert strings to idents by using ltac2. However, I’m not quite sure how to do it in the reversed way (say, converting idents to strings).

More specifically, I’m trying to do something like (fun (x y: ty) => ...) with

Goal True.
Proof.
  match constr:((fun (x y: nat) => x)) with 
  | (fun (name:_) => _) => some_tac (ident_to_string name)
  end.

Now I have an intropattern name, and idtac name prints x. The problem is, this some_tac can only accept a string. Is there any way to write a ident_to_string ltac to magically acquire string "x" from name?

2

This file from Kôika is independent from the rest of the project and implements that transformation.

There’s a function ident_to_string that you can use:

Require Import IdentToString.

Goal True.
  ltac1:(match constr:((fun (x y: nat) => x)) with
         | (fun (name:_) => _) => pose (ident_to_string name) as s
         end).
  (* s := "x"%string : string *)

We plan to release it as a separate library but we haven’t gotten around to it yet.

2 Likes
3

This snippet of code works perfectly! Thanks!