From 54316fabb45469e0b96bc697228858527dced94f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 21 Aug 2021 16:39:18 -0700 Subject: [PATCH] feat: add `nonrec` parser --- src/Lean/Parser/Command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 2f25bed2a6..f21a840792 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -32,7 +32,8 @@ def visibility := «private» <|> «protected» def «noncomputable» := leading_parser "noncomputable " def «unsafe» := leading_parser "unsafe " def «partial» := leading_parser "partial " -def declModifiers (inline : Bool) := leading_parser optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial» +def «nonrec» := leading_parser "nonrec " +def declModifiers (inline : Bool) := leading_parser optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional («partial» <|> «nonrec») def declId := leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}") def declSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.typeSpec def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType