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

feat: more pp tweaks

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-02 17:40:18 +02:00
parent e777478aa1
commit 88164a5e91
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -64,8 +64,8 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
@[builtinCommandParser] def «section» := parser! "section " >> optional ident
@[builtinCommandParser] def «namespace» := parser! "namespace " >> ident
@[builtinCommandParser] def «end» := parser! "end " >> optional ident
@[builtinCommandParser] def «variable» := parser! "variable " >> Term.bracketedBinder
@[builtinCommandParser] def «variables» := parser! "variables " >> many1 Term.bracketedBinder
@[builtinCommandParser] def «variable» := parser! "variable" >> Term.bracketedBinder
@[builtinCommandParser] def «variables» := parser! "variables" >> many1 Term.bracketedBinder
@[builtinCommandParser] def «universe» := parser! "universe " >> ident
@[builtinCommandParser] def «universes» := parser! "universes " >> many1 ident
@[builtinCommandParser] def check := parser! "#check " >> termParser

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

@ -124,8 +124,8 @@ def simpleBinder := parser! many1 binderIdent
@[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
def matchAlt : Parser :=
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
sepBy1 termParser ", " >> darrow >> termParser
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ ppGroup $
ppGroup (sepBy1 termParser ", " >> darrow) >> termParser
def matchAlts (optionalFirstBar := true) : Parser :=
parser! withPosition $
@ -161,7 +161,7 @@ def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
@[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optional ";\n" >> termParser
def attrArg : Parser := ident <|> strLit <|> numLit
-- use `rawIdent` because of attribute names such as `instance`
def attrInstance := parser! rawIdent >> many (ppSpace >> attrArg)
def attrInstance := ppGroup $ parser! rawIdent >> many (ppSpace >> attrArg)
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", "
@[builtinTermParser] def «letrec» :=