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

fix: indent structure fields

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-08 21:37:31 +01:00 • committed by Sebastian Ullrich
parent 316fa81042
commit f5a2562575
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

@ -81,7 +81,7 @@ def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >>
def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault)
def structFields := leading_parser manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
def structFields := leading_parser manyIndent (ppLine >> checkColGe >> ppGroup (structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
def structCtor := leading_parser atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
def structureTk := leading_parser "structure "
def classTk := leading_parser "class "