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

fix: print line before deriving

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-09 18:27:31 +01:00 • committed by Sebastian Ullrich
parent 5d25df1a69
commit b176efefca
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -74,7 +74,7 @@ def «example» := leading_parser "example" >> ppIndent declSig >> declVa
def inferMod := leading_parser atomic (symbol "{" >> "}")
def ctor := leading_parser "\n| " >> ppIndent (declModifiers true >> ident >> optional inferMod >> optDeclSig)
def derivingClasses := sepBy1 (group (ident >> optional (" with " >> Term.structInst))) ", "
def optDeriving := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
def optDeriving := leading_parser optional (ppLine >> 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 >> ppIndent optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> ppIndent optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) >> ")"