Hugo Herbelin (Nov 25 2020 at 19:16): Hugo Herbelin (Nov 25 2020 at 19:16):There is something wrong with automatic implicit arguments in Context or sequence of variables (in the style of #4017), namely that they are dependent on the progresses made by unification. Should automatic implicit arguments be deactivated in sequences (even if activated after the sequence), activated on the syntactically available part of the expressions (even again if reactivated using the full information after the sequence):
Section A.
Set Implicit Arguments.
Variables (f1 : _) (x1 : f1 0 (eq_refl 0) = 0).
Variables (f2 : forall x:nat, x=x->nat) (x2 : f2 (eq_refl 0) = 0).
About f1. (* f1 : forall [x : nat], x = x -> nat *)
About f2. (* f2 : forall [x : nat], x = x -> nat *)
Then, the same question can be asked for:
Set Implicit Arguments.
Lemma foo1 (f1 : _) (x1 : f1 0 (eq_refl 0) = 0) : True.
Fail Lemma foo2 (f2 : forall n:nat, n=n->nat) (x2 : f2 (eq_refl 0) = 0) : True.
Lemma foo2 (f2 : forall n:nat, n=n->nat) (x2 : f2 0 (eq_refl 0) = 0) : True.
Last updated: Nov 29 2023 at 05:01 UTC