Hi, is it possible to convert a Ltac1 integer into a Ltac2 integer? I don't see a function for that in https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Ltac1.v .
Concretely, is there something I can fill in for
??? in the example below to make it print the argument
Tactic Notation "print_int" int(n) := let r := ltac2:(n |- Message.print (Message.of_int (??? n))) in r n.
Indeed, there is no function for that, but it should be easy to add (either in the Ltac2 standard library, or via a plugin). One possible workaround is to rely on a constr instead of an integer I guess, but whether that is good enough depends on your actual use-case.
Last updated: Nov 29 2023 at 22:01 UTC