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

view this post on Zulip Notification Bot (Sep 26 2022 at 15:12):

Jason Gross has marked this topic as resolved.

Last updated: May 28 2023 at 16:30 UTC