max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: return value is optional

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-02 18:09:42 -07:00
parent 137b9efd42
commit c40ec0128d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Do.lean
View file

@ -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