It is not yet clear to me how I should declare the arguments of a
Coq tactic which is based upon an
Look at the following code (I leave the tactic
mytac opaque, I doubt its body matters here).
Elpi Tactic mytac. (* snip *) solve (goal _ _ _ _ [trm M, int N] as G) GL : (* snip *) Elpi Typecheck. Tactic Notation "mytac" constr(l) integer(n) := elpi mytac (l) ltac_int(n). (* this also fails when I remove ltac_int *) Goal forall (n : nat), n = 3 -> 2 +2 = 5. intros n. elpi mytac (match 2 with | 0 => true | S k => false end) 0. Fail mytac (match 2 with | 0 => true | S k => false end) 0.
The last instruction gives:
The command has indeed failed with message:
The elpi tactic mytac failed without giving a specific error message. Please
report this inconvenience to the authors of the program.
In this case, how should I declare the
Last updated: Feb 05 2023 at 13:02 UTC