Stream: Ltac2

Topic: Constr mapping


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

I'm looking at EConstr.{map,map_with_binders,iter,iter_with_full_binders,fold,fold_with_binders (why does only iter have a full_binders version? What's up with the difference?), and wondering if I should expose them all in Ltac2.Constr.Unsafe. (I'm currently wanting to use Constr.map_with_binders.) Thoughts?


Last updated: Jan 31 2023 at 10:01 UTC