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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-02 15:48:46 -07:00
parent 35e401e915
commit e8edd810de
2 changed files with 1437 additions and 1076 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
stage0/src/Lean/Parser/Do.lean generated
View file

@ -22,7 +22,7 @@ def leftArrow : Parser := unicodeSymbol " ← " " <- "
@[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
def doSeqIndent := many1Indent $ doElemParser >> optional "; "
def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
def doSeqBracketed := parser! "{" >> withoutPosition (many1 (doElemParser >> optional "; ")) >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
@ -79,9 +79,9 @@ def doCatchMatch := parser! "catch " >> doMatchAlts
def doFinally := parser! "finally " >> doSeq
@[builtinDoElemParser] def doTry := parser! "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
@[builtinDoElemParser] def «break» := parser! "break"
@[builtinDoElemParser] def «continue» := parser! "continue"
@[builtinDoElemParser] def «return» := parser!:leadPrec "return " >> termParser
@[builtinDoElemParser] def doBreak := parser! "break"
@[builtinDoElemParser] def doContinue := parser! "continue"
@[builtinDoElemParser] def doReturn := parser!:leadPrec "return " >> termParser
@[builtinDoElemParser] def doDbgTrace := parser!:leadPrec "dbgTrace! " >> termParser
@[builtinDoElemParser] def doAssert := parser!:leadPrec "assert! " >> termParser

2505
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff