chore: remove unnecessary workaround

It is not needed anymore after we fixed the `app` parser
This commit is contained in:
Leonardo de Moura 2020-02-03 20:23:19 -08:00
parent 6be9a73e51
commit 1f359b9844
2 changed files with 5 additions and 1 deletions

View file

@ -116,7 +116,7 @@ def doExpr := parser! termParser
def doElem := doLet <|> doId <|> doPat <|> doExpr
def doSeq := sepBy1 doElem "; "
def bracketedDoSeq := parser! "{" >> doSeq >> "}"
@[builtinTermParser] def liftMethod := parser! checkRBPGreater (appPrec-1) "expected parentheses monad lift operator" >> leftArrow >> termParser
@[builtinTermParser] def liftMethod := parser! leftArrow >> termParser
@[builtinTermParser] def «do» := parser! "do " >> (bracketedDoSeq <|> doSeq)
@[builtinTermParser] def not := parser! symbol "¬" 40 >> termParser 40

View file

@ -3,3 +3,7 @@ new_frontend
def tst : IO (Option Nat) := do
x? : Option Nat ← pure none;
pure x?
def tst2 (x : Nat) : IO (Option Nat) := do
x? : Option Nat ← pure x;
if x?.isNone then pure (x+1) else pure x?