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

fix: update builtin precedences for |>. and macroDollarArg

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-22 11:50:32 -08:00
parent 18aee9de30
commit cc34733e52
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -195,7 +195,7 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def explicitUniv : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
@[builtinTermParser] def namedPattern : TrailingParser := tparser! checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
@[builtinTermParser] def pipeProj := tparser!:0 " |>. " >> (fieldIdx <|> ident)
@[builtinTermParser] def pipeProj := tparser!:10 " |>. " >> (fieldIdx <|> ident)
@[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
@ -211,7 +211,7 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
def macroArg := termParser maxPrec
def macroDollarArg := parser! "$" >> termParser 0
def macroDollarArg := parser! "$" >> termParser 10
def macroLastArg := macroDollarArg <|> macroArg
-- Macro for avoiding exponentially big terms when using `STWorld`