search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.75k stars 428 forks source link

`parseQuotWithCurrentStage` works reliably only for builtin parsers #6118

Open Kha opened 1 week ago

Kha commented 1 week ago

For non-builtin parsers, the option is ignored unless they are called directly by name: `(thisParserWillBeTakenFromCurrentStage| ...)

Kha commented 4 days ago

Note: this only applies to interpreter.prefer_native=true as otherwise the parser is of course always taken from the current stage