quote4

quote4 copied to clipboard

Since `Simproc.ofQ` is a higher order function, it's good to inline or specialize it.

JovanGerb

This will require a mathlib patch

eric-wieser

eric-wieser

misc/examples.lean currently PANICs

1

Either diagnose and fix, or at very least comment out.

kim-em

eric-wieser

When quoted data is declared using the `variable` command, occurrence highlighting picks up a lot of irrelevant stuff. ### Lean version ``` Lean 4.22.0-rc3 Target: arm64-apple-darwin23.6.0 macOS ``` ### `quote4`...

Vtec234

fix: make goto definition work on quoted variables

7

This follows up on #88 This also fixes semantic highlighting: 

eric-wieser