diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index e69297bb2c..c10003ca89 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -85,7 +85,7 @@ def doFinally := parser! "finally " >> doSeq @[builtinDoElemParser] def doBreak := parser! "break" @[builtinDoElemParser] def doContinue := parser! "continue" -@[builtinDoElemParser] def doReturn := parser!:leadPrec "return " >> optional termParser +@[builtinDoElemParser] def doReturn := parser!:leadPrec withPosition ("return " >> optional (checkLineEq >> termParser)) @[builtinDoElemParser] def doDbgTrace := parser!:leadPrec "dbgTrace! " >> ((interpolatedStr termParser) <|> termParser) @[builtinDoElemParser] def doAssert := parser!:leadPrec "assert! " >> termParser diff --git a/tests/lean/run/returnOptIssue.lean b/tests/lean/run/returnOptIssue.lean new file mode 100644 index 0000000000..ed9b6df1ff --- /dev/null +++ b/tests/lean/run/returnOptIssue.lean @@ -0,0 +1,8 @@ +#lang lean4 + +def f (x : Nat) : IO Unit := do +if x > 10 then + return +throw $ IO.userError "x ≤ 10" + +#eval f 11