quote4
quote4 copied to clipboard
leanprover-community
Intuitive, type-safe expression quotations for Lean 4.
Consider the following program: ```lean def abc : Q(Type) := let e : Expr := Expr.const `abc [] let f : Q(Type) := Expr.const ``Nat [] q(sorry) ``` Then hovering...
quote4 is amazing at pattern matching in hypotheses and the goal. Thank you so much for creating this library. It is already a huge help. I was wondering if would...
I'm running into a very weird error when using Qq, where the presence of ```lean4 let args := a :: args ``` Causes an `unknown free variable '_uniq.419'` error in...
IIUC, when writing `q($n)` for, say `n : Nat`, it automatically translates `$n` into `ToExpr.toExpr n`. This mechanism doesn't seem to work when we have an antiquotation of generic type...
This makes it slightly clearer what is going on here.
Universe variables are now parsed in `foo.{u,v}` terms, making `foo.{$u,$v}` legal.
lakefile: `require Qq from git "https://github.com/leanprover-community/quote4" @ "master" ` imported and opened Qq fine; simple examples work but: `def betterApp {α : Q(Sort u)} {β : Q($α → Sort v)}...
Amazing library, thanks so much for the amazing work. We are just attempting to update and we are having a problem: In https://github.com/leanprover-community/quote4/pull/49 the option was added `set_option linter.constructorNameAsVariable false...
Add a way to opt into pure structural `Expr` equality for `~q`-style pattern matching instead of definitional equality. Currently `~q` silently unfolds definitions and performs expensive reductions when matching, which...
Metadata
Owner
Metadata
Intuitive, type-safe expression quotations for Lean 4.