max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/parser/command): add class inductive

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-15 15:24:26 -07:00
parent 65edaa12a3
commit 262e83bbc8
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/parser/command.lean
View file

@ -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