Stream: Ltac2

Topic: Differences between Ltac2 constr context and usual context

Patrick Nicodemus (Jan 21 2024 at 01:25):

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?

Patrick Nicodemus (Jan 21 2024 at 02:07):

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