Stream: Coq devs & plugin devs

Topic: EConstr.fold


view this post on Zulip Jason Gross (Sep 26 2022 at 05:57):

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?

view this post on Zulip Gaƫtan Gilbert (Sep 26 2022 at 08:00):

EConstr.fold does not recurse, it calls the f argument on the immediate subterms


Last updated: Feb 05 2023 at 20:03 UTC