Hello,

Out of curiosity, how should I do to write an `Elpi`

tactic which returns a term? As a toy example, a tactic which takes a `Coq`

term `t`

and outputs the pair `( t , t )`

?

All tactics return a term, in the sense that they are called on a goal (a type) and they inhabit it. Your question seems like: "how do I write a tactics which proves `A -> A /\ A`

". What am I missing?

Well, I'm looking for a tactic which returns a term that I can use. So that if `foo`

is my `elpi`

tactic which takes a term `t`

and outputs `( t , t )`

and `x`

is a term in the context, I can write something like :

```
let na := fresh in let xx:= foo x in pose x as na.
```

Hi. An Elpi tactic cannot directly return a term, it more or less takes the proof state and has the ability to modify it with various API calls, but one of them is `refine`

. Among other features, it lets you pose a term in the context.

IIUC, the line you posted is roughly equivalent to

```
refine (let na := foo x in _).
```

If you write an Elpi predicate taking any term `x`

and generating the content of what you currently call `foo x`

, in 2 lines you can have a tactic that takes `x`

as an argument, computes the output term, and calls `refine`

to add it to the context.

```
solve (goal _ _ GoalTy _ [trm X] as Goal) NewGoals :-
compute-foo X FooX,
refine (let _ _ FooX (t\ {{ _ : lp:GoalTy }})) Goal NewGoals.
```

NB: I just made up this code on Zulip but I know this technique works, I have used it in Trakt ;)

Thanks @Enzo Crance !

Thanks @Enzo Crance you were faster than me! Since I was too writing a solution, here it is:

```
Elpi Tactic double.
Elpi Accumulate lp:{{
solve (goal _ _ _ _ [trm X] as G) GL :-
refine {{ ( lp:X , lp:X ) }} G GL.
}}.
Elpi Typecheck.
Tactic Notation "foo" uconstr(x) := elpi double ltac_term:(x).
Goal forall x : nat, True.
Proof.
intro x.
let xx := foo x in
pose (ltac:(xx)) as na.
(* in the context you now have na : nat * nat := (x, x) *)
```

Last updated: Feb 04 2023 at 02:03 UTC