# Convert ident to string in ltac

**URL:** <https://discourse.rocq-prover.org/t/convert-ident-to-string-in-ltac/1159>\
**Category:** Using Rocq\
**Created:** [December 16, 2020, 12:52am UTC](https://discourse.rocq-prover.org/t/convert-ident-to-string-in-ltac/1159 "2020-12-16T00:52:04Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![LightQuantum](https://avatars.discourse-cdn.com/v4/letter/l/c6cbf5/32.png) [@LightQuantum](https://discourse.rocq-prover.org/u/LightQuantum)\
**Post date:** [December 16, 2020, 12:52am UTC](https://discourse.rocq-prover.org/t/convert-ident-to-string-in-ltac/1159/1 "2020-12-16T00:52:04Z")

</div>

This problem is partly related to [coq/7922](https://github.com/coq/coq/issues/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

```coq
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`?

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [December 16, 2020, 2:19am UTC](https://discourse.rocq-prover.org/t/convert-ident-to-string-in-ltac/1159/2 "2020-12-16T02:19:44Z")

</div>

[This file](https://github.com/mit-plv/koika/blob/master/coq/IdentParsing.v) 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:

```auto
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.

---

<div class="post-metadata">

**Author:** ![LightQuantum](https://avatars.discourse-cdn.com/v4/letter/l/c6cbf5/32.png) [@LightQuantum](https://discourse.rocq-prover.org/u/LightQuantum)\
**Post date:** [December 16, 2020, 8:47pm UTC](https://discourse.rocq-prover.org/t/convert-ident-to-string-in-ltac/1159/3 "2020-12-16T20:47:33Z")

</div>

This snippet of code works perfectly! Thanks!