New blog post on quasiquotation with binders (via hygiene)

Stream: general

[David Thrane Christiansen]

I just put up a post on the Lean blog, showing a fun trick that can be done with hygiene and scopes.

[Kim Morrison]

• in the "Environment" section, it looks like you define def LocalEnv v := List (LName × v) and could use it in structure Env but then surprisingly don't?
• when I wanted to tell you about this, I tried to find a way to link to the "Environment" section, but couldn't see a way.

[David Thrane Christiansen]

Thanks! I can't use them in Env because it makes the kernel reject the definition of Val later on :⁠-⁠(

[David Thrane Christiansen]

Permalinks to sections are on the way :⁠-⁠)

[Asei Inoue]

Here is a view from mobile (iphone15).
title is too big..?

IMG_0067.jpeg