From 1f359b984483a679a4d30782e2bd846fea71ed0b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Feb 2020 20:23:19 -0800
Subject: [PATCH] chore: remove unnecessary workaround

It is not needed anymore after we fixed the `app` parser
---
 src/Init/Lean/Parser/Term.lean      | 2 +-
 tests/lean/run/LiftMethodIssue.lean | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean
index 32e0cd61db..18e80a7d6c 100644
--- a/src/Init/Lean/Parser/Term.lean
+++ b/src/Init/Lean/Parser/Term.lean
@@ -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
diff --git a/tests/lean/run/LiftMethodIssue.lean b/tests/lean/run/LiftMethodIssue.lean
index a074a99193..1074ddad9d 100644
--- a/tests/lean/run/LiftMethodIssue.lean
+++ b/tests/lean/run/LiftMethodIssue.lean
@@ -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?