Lean.Meta.forallTelescope and Lean.Meta.forallMetaTelescope

Stream: metaprogramming / tactics

[Geoffrey Irving]

I want to do some analysis for each of the hypotheses of a theorem. I'd like to use information about the binders, in particular filtering down to non-implicit hypotheses. However, the options are

1. Lean.Meta.forallTelescope: Does the work of cleaning up introduced mvars, but doesn't provide binder information.
2. Lean.Meta.forallMetaTelescope: Returns binders, but doesn't do mvar cleanup.

Presumably I should use (2) but do the cleanup myself. How do I do that? Is there a reason the API is nonuniform in this way?

[Jannis Limperg]

Use (1). The Exprs in the Array are guaranteed to be FVarIds (this should be cleaned up), so you can getDecl their LocalDecls and obtain the BinderInfo from there.

[Geoffrey Irving]

Ah, thank you!