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

fix: field syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-17 10:12:43 -07:00
parent b5dc185e70
commit a1fc824336
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Parser/Command.lean
View file

@ -57,9 +57,9 @@ def inferMod := parser! try ("{" >> "}")
def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many ctor
def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
def structExplicitBinder := parser! try (declModifiers >> "(") >> many ident >> optional inferMod >> declSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! try (declModifiers >> "{") >> many ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! try (declModifiers >> "[") >> many ident >> optional inferMod >> declSig >> "]"
def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> declSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
def structCtor := parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
def structureTk := parser! "structure "