Stream: Elpi users & devs

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

Enzo Crance (Sep 19 2022 at 14:13):

Something like this?

Tactic Notation "mytac" constr(l) integer(n) := elpi mytac ltac_term:(l) ltac_int:(n).

Pierre Vial (Sep 19 2022 at 14:16):

Yes, it does work, though, for some reason, when the tactic had only one argument (aka l), it wasn't necessary to wrise ltac_term: before l on the right-hand side

Notification Bot (Sep 19 2022 at 14:18):

Pierre Vial has marked this topic as resolved.

Enrico Tassi (Sep 19 2022 at 19:09):

The problem is the missing : after ltac_int, not the extra ltac_term.

Last updated: Feb 04 2023 at 01:03 UTC