Tomaz Gomes (Sep 11 2024 at 15:07): Tomaz Gomes (Sep 11 2024 at 15:07):Hi,
I am trying to write a tactic in Elpi that should introduce a variable in the context whose name is given by the user. I tried to follow the documentation but I am stuck at this point:
From elpi Require Import elpi.
Ltac elpi_pose foo := pose (foo := 42).
Elpi Tactic example_elpi.
Elpi Accumulate lp:{{
solve (goal _ _ _ _ [str Name] as G) GL :-
coq.ltac.call "elpi_pose" [str Name] G GL.
}}.
Elpi Typecheck.
Tactic Notation "example" ident(f) :=
elpi example_elpi ltac_string:(f).
Goal True.
example bar.
Abort.
With this error message:
Debug: Ltac variable foo is bound to "bar" which cannot be coerced to a fresh identifier.
File "tmp.v", line 19, characters 2-14:
Error: The elpi tactic/command example_elpi failed without giving a specific error message. Please report this inconvenience to the authors of the program.
There are some examples in the coq-elpi github space. This one implements some basic tactics, like intro:
Elpi Tactic intro.
Last updated: Oct 13 2024 at 01:02 UTC