From c40ec0128d260e341cb8b7d3c310b467401fa3e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Oct 2020 18:09:42 -0700 Subject: [PATCH] fix: `return` value is optional --- src/Lean/Parser/Do.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 2329db14dd..f680be6382 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -81,7 +81,7 @@ def doFinally := parser! "finally " >> doSeq @[builtinDoElemParser] def doBreak := parser! "break" @[builtinDoElemParser] def doContinue := parser! "continue" -@[builtinDoElemParser] def doReturn := parser!:leadPrec "return " >> termParser +@[builtinDoElemParser] def doReturn := parser!:leadPrec "return " >> optional termParser @[builtinDoElemParser] def doDbgTrace := parser!:leadPrec "dbgTrace! " >> termParser @[builtinDoElemParser] def doAssert := parser!:leadPrec "assert! " >> termParser