From cfb5d34dd3f1da589b3bf83c49eb3d7aaaef0913 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 21 Jul 2021 00:57:33 -0700 Subject: [PATCH] fix: parser arity --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 2c7d9e5777..403ab2532e 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -45,7 +45,7 @@ def «axiom» := leading_parser "axiom " >> declId >> declSig def «example» := leading_parser "example " >> declSig >> declVal def inferMod := leading_parser atomic (symbol "{" >> "}") def ctor := leading_parser "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig -def derivingClasses := sepBy1 (ident >> optional (" with " >> Term.structInst)) ", " +def derivingClasses := sepBy1 (group (ident >> optional (" with " >> Term.structInst))) ", " def optDeriving := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> derivingClasses) def «inductive» := leading_parser "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving def classInductive := leading_parser atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving