Stream: Elpi users & devs

Topic: [beginner] Arguments of a tactic defined with `Elpi`


view this post on Zulip Pierre Vial (Sep 19 2022 at 13:59):

Hi,
It is not yet clear to me how I should declare the arguments of a Coq tactic which is based upon an Elpi tactic.
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 Coq tactic mytac?


Last updated: Feb 05 2023 at 13:02 UTC