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: Dec 01 2023 at 07:01 UTC