Version of `mkLambdaFVars` taking an array of binderinfos

Stream: metaprogramming / tactics

[Calle Sönne]

Is there a version of mkLambdaFVars which takes an array of binderinfos (of the same length as the array of metavariables to abstract) such that the i:th index of the array of binderinfos gives the binderinfo for the i:th metavariable? Currently, I am using quite an awkward workaround by applying mkLambdaFVars to one metavariable at a time, so that I can control the binderinfo at each step.

[Jannis Limperg]

I was looking for this as well and didn't find it. Shouldn't be too hard to write it yourself by copy-pasting the mkLambdaFVars code.

[Kyle Miller]

If it were for fvars, you would use docs#Lean.Meta.withNewBinderInfos to change the binder infos and then use mkLambdaFVars from within that context.

[Kyle Miller]

I think the API tends to work better with fvars — do you mind if I ask why you're abstracting mvars? Sometimes I've noticed people reaching for meta telescopes when they could be using the other telescope functions.

[Jannis Limperg]

This was in the context of #metaprogramming / tactics > Specializing function at unknown point (and univese issues). It should definitely be possible to solve this with an fvar telescope instead, but it would have been harder in other ways. Specifically, we wanted to replace an fvar with a particular value and with fvars, we would have had to make this replacement everywhere in later fvars whereas with mvars this is free.

[Calle Sönne]

Yes exactly, I was not sure how to do that part with FVars. When starting to write that code I was actually constantly switching between using forallTelescope and forallMetaTelescope, and I ended up making the most progress with the latter.