From 8fd6870931d354270442f95bfcfe2fa055be8098 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Dec 2020 18:58:44 -0800 Subject: [PATCH] fix: `optDeriving` parser --- 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 1a3a816cee..0f7edc7180 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -47,7 +47,7 @@ def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal def inferMod := parser! atomic (symbol "{" >> "}") def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig -def optDeriving := parser! optional ("deriving " >> sepBy1 ident ", ") +def optDeriving := parser! optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving def classInductive := parser! atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"