Stream: Ltac2

Topic: Constr mapping

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: Oct 12 2024 at 13:01 UTC