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

fix: add missing precedence to liftMethod and remove unnecessary precedence from doLet

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-04 15:43:46 -07:00
parent b3a8d417b2
commit 400aa435f3
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

@ -126,14 +126,14 @@ def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl
@[builtinTermParser] def «let!» := parser! [leadPrec] "let! " >> letDecl >> "; " >> termParser
def leftArrow : Parser := unicodeSymbol " ← " " <- "
def doLet := parser! [leadPrec] "let ">> letDecl
def doLet := parser! "let ">> letDecl
def doId := parser! try (ident >> optType >> leftArrow) >> termParser
def doPat := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
def doExpr := parser! termParser
def doElem := doLet <|> doId <|> doPat <|> doExpr
def doSeq := sepBy1 doElem "; "
def bracketedDoSeq := parser! [appPrec] "{" >> doSeq >> "}"
@[builtinTermParser] def liftMethod := parser! leftArrow >> termParser
@[builtinTermParser] def liftMethod := parser! [0] leftArrow >> termParser
@[builtinTermParser] def «do» := parser! [leadPrec] "do " >> (bracketedDoSeq <|> doSeq)
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec