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

chore: switch to attrParam

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 17:39:30 -08:00
parent ac440aa6ea
commit 6985223a55
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -18,7 +18,7 @@ builtin_initialize
registerBuiltinDynamicParserAttribute `prioParser `prio
builtin_initialize
registerBuiltinParserAttribute `builtinAttrParamParser `attrParam (leadingIdentAsSymbol := true)
registerBuiltinParserAttribute `builtinAttrParamParser `attrParam
registerBuiltinDynamicParserAttribute `attrParamParser `attrParam
@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
@ -176,12 +176,11 @@ def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
@[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optSemicolon termParser
@[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser
def attrArg : Parser := ident <|> strLit <|> numLit -- attrParamParser
def «scoped» := parser! "scoped "
def «local» := parser! "local "
def attrKind := parser! optional («scoped» <|> «local»)
-- use `rawIdent` because of attribute names such as `instance`
def attrInstance := ppGroup $ parser! attrKind >> rawIdent >> many (ppSpace >> attrArg)
def attrInstance := ppGroup $ parser! attrKind >> rawIdent >> many (ppSpace >> attrParamParser maxPrec)
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", "