Looking for "Quasiquotation with Binders" as elaborator

Stream: new members

[Nate Sandy]

Hi!
In this blog post Quasiquotation with Binders: A Lean Metaprogramming Example, David mentions at the end:

An upcoming post will demonstrate some techniques for associating more information with bound variables, moving from a macro-based implementation to an elaborator, which uses the compiler's API to translate terms directly to Lean's core type theory.

I think this is precisely what I'll need to do for my DSL, but it seems that upcoming post does not exist (yet?), so I'm looking for examples of how to do this. So far I've been following Embedding DSLs By Elaboration - Metaprogramming in Lean 4, but while that book shows how to do binders with macros, the elaborated DSL doesn't have binders. I've also seen Parametric Higher-Order Abstract Syntax - Lean Documentation Overview, but I'm not sure whether that is what I need.

So, essentially I am looking for examples and/or tutorials on elaborators of DSLs that have bindings. Any pointers are much appreciated! Maybe a small DSL that uses this technique would suffice to learn by example, but I couldn't find one yet.

[Kyle Miller]

Maybe it's worth looking at Lean's own binder elaboration, which is all in src/Lean/Elab/Binders.lean

The key parts are withLocalDecl for adding variables to the local context, addLocalVarInfo for registering syntax responsible for the local variable, and, elsewhere, functions to create foralls/lambdas/lets (mkForallFVars, mkLambdaFVars, mkLetFVars), closing the expressions.

[Nate Sandy]

Thanks for the pointers Kyle!

I also realized that the Metaprogramming book has some information about binders, that I initially missed: https://leanprover-community.github.io/lean4-metaprogramming-book/main/04_metam.html?highlight=mklam#lambdas-and-foralls

I'll also look into Lean's elaboration, it definitely helps to know what functions to search for. I think with this I can continue for now :)