e1d15946f7
This PR enables the elaboration of theorem bodies, i.e. proofs, to happen in parallel to each other as well as to other elaboration tasks. Specifically, to be eligible for parallel proof elaboration, * the theorem must not be in a `mutual` block * `deprecated.oldSectionVars` must not be set * `Elab.async` must be set (currently defaults to `true` in the language server, `false` on the cmdline) To be activated for downstream projects (i.e. in stage 1) pending further Mathlib validation.
10 lines
616 B
Text
10 lines
616 B
Text
syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
|
|
[Elab.command] @[term_parser 1000]
|
|
def «termFoo*_» : Lean.ParserDescr✝ :=
|
|
ParserDescr.node✝ `«termFoo*_» 1022
|
|
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
|
|
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
|
|
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
|
|
(ParserDescr.symbol✝ ", ") Bool.false✝)))
|
|
[Elab.command] syntax "foo" ("*" <|> term,+) : term
|
|
[Elab.command]
|