Qq and local variables

Stream: lean4

[Jakob von Raumer]

Is it possible to use Qq with local variables, e.g. let-bound variables in a do-block?

[Gabriel Ebner]

Can you be a bit more specific? I believe the answer is yes in any way that I can think of: you can use quoted expression in do-blocks, antiquotations can refer to quoted expressions introduced by bind, quoted expressions can be free variables, etc.

[Gabriel Ebner]

Quote4 does not keep track of the local context however. Nothing prevents you from taking a free variable out of a forallTelescope.

[Jakob von Raumer]

Okay, I'll try and come up with a small example