From 702ceb7a3fb169e25ea2ed9d3b98ba45521bf185 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Oct 2020 05:58:35 -0700 Subject: [PATCH] fix: `return` optional result cc @Kha --- src/Lean/Parser/Do.lean | 2 +- tests/lean/run/returnOptIssue.lean | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/returnOptIssue.lean 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