It seems to me that EConstr.fold will only normalize evars in the head position, and will otherwise fold over the instances of evars that have been instantiated. But
Require Import Ltac2.Ltac2. Require Import Ltac2.Printf. Set Printing Existential Instances. Goal forall n : Set, exists e : Set, True. intro n; eexists ?[e]. let c := '(id ?e) in let __ := '(ltac:(unify ?e nat; exact I)) in let s := Fresh.Free.of_constr c in let n := Fresh.fresh s @n in printf "%t - %t" c (Constr.Unsafe.make (Constr.Unsafe.Var n)). (* (id nat) - n *)
Suggests that this is not the case. What am I missing? How is it that
Ltac2.Fresh.Free.of_constr picks up the evar-normalized instances in places other than the head positions?
EConstr.fold does not recurse, it calls the
f argument on the immediate subterms
Jason Gross has marked this topic as resolved.
Last updated: Dec 07 2023 at 06:38 UTC