## Stream: Elpi users & devs

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

#### 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`?

#### 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: Jun 06 2023 at 23:01 UTC