More granular binder info control in `mkForallFvars`

Stream: metaprogramming / tactics

[Robin Carlier]

When deconstructing a forall expression using forallMetaTelescope, the binder infos are extracted and returned in an array. When reconstructing such an expression using mkForallFVars, the argument binderInfoForMVars only accepts a single BinderInfo, and so every binders in the reconstructed expressions are the same.
Is there a relatively easy way around this that would let me reconstruct a forall expression in such a way that I can specify possibly different binder infos for every var?

[Robin Carlier]

(For reasons I don’t fully understand, it looks like mapForallTelescope is able to reconstruct the correct binders, despite using at first glance mkForallFVars behind the scene. I would be glad to have an explanation about the why, is it because it somehow tries to re-cast the result into the expected type of the telescope, which bundles the binder infos?)

[Jovan Gerbscheid]

mapForallTelescope uses forallTelescope, not forallMetaTelescope. The difference is that forallTelescope introduces free variables, while forallMetaTelescope introduces meta variables. Free variables store their BinderInfo in the environment. You might need to use free variables instead of metavariables, depending on your use case.

[Robin Carlier]

Thanks for the explanation.