From 262e83bbc86b37d041908452f6b828b54b82f884 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Jul 2019 15:24:26 -0700 Subject: [PATCH] fix(library/init/lean/parser/command): add `class inductive` --- library/init/lean/parser/command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index 223b06e8e3..369570f497 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -57,6 +57,7 @@ def strictInferMod := parser! try ("(" >> ")") def inferMod := relaxedInferMod <|> strictInferMod def introRule := parser! " | " >> ident >> optional inferMod >> optDeclSig def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many introRule +def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many introRule def structExplicitBinder := parser! "(" >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" def structImplicitBinder := parser! "{" >> many ident >> optional inferMod >> optDeclSig >> "}" def structInstBinder := parser! "[" >> many ident >> optional inferMod >> optDeclSig >> "]" @@ -68,7 +69,7 @@ def «extends» := parser! " extends " >> sepBy1 termParser ", " def «structure» := parser! (structureTk <|> classTk) >> declId >> many Term.bracktedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields @[builtinCommandParser] def declaration := parser! -declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> «structure») +declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure») @[builtinCommandParser] def «section» := parser! "section " >> optional ident @[builtinCommandParser] def «namespace» := parser! "namespace " >> ident