Using `BinderView` and `toBinderViews`

Stream: metaprogramming / tactics

[William Sørensen]

Hi I am writing some code that uses BinderViews quite prevalently. Is this good practice? I see that toBinderViews is private, but it is also extremely useful to work with. Are there any better alternatives? What's done in lean upstream?

[Anand Rao Tadipatri]

It depends on the use case, but it may be better to work with Exprs instead of Syntax if it's feasible. Some meta-level functions that make it easier to deal with binders include docs#Lean.Meta.forallMetaTelescope and docs#Lean.Meta.withLocalDecl.

[William Sørensen]

I think working with syntax here would be so much easier as i am constructing inductive datatypes and then elaborating this. For the project, the code is already pretty far but using toBinderViews which is quite painful