Stream: Ltac2

Topic: Convert Ltac1 integer to Ltac2 integer

MackieLoeffel (May 14 2023 at 12:15):

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 n?

  Tactic Notation "print_int" int(n) :=
    let r := ltac2:(n |- Message.print (Message.of_int (??? n))) in
    r n.

Rodolphe Lepigre (May 14 2023 at 14:36):

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: Oct 12 2024 at 13:01 UTC