```
Record myrec := {
P : nat -> Type;
E {n : nat} : P n;
x {n : nat}: P n := E
}.
```

This works.

```
Record myrec := {
P : nat -> Type;
E {n : nat} : P n;
x {n : nat}: P n := ltac2:(refine 'E)
}.
```

This raises the following error:

```
Error:
In environment
myrec : Type
P : nat → Type
E : ∀ n : nat, P n
n : nat
The term "E" has type "∀ n : nat, P n"
while it is expected to have type "P n".
```

When we pass to the Ltac2 constr context it forgets that E is supposed to have its arguments as implicit. I have to write E _. This is inconvenient but not too difficult to work around. Is this a bug? Or are there good reasons to have this distinction?

```
Ltac2 pf f g :=
exact (&c $f $g).
Theorem claim : forall a1 a2 a3, B a1 a2 -> B a2 a3 -> B a1 a3.
Proof.
intros a1 a2 a3 f g.
Fail pf &f &g.
```

Is there a way to set a convention where it just takes the implicit arguments at the moment it's "compiled"/internalized?

Last updated: Oct 12 2024 at 12:01 UTC