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

chore: do syntax adjustments

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-03 07:33:18 -07:00
parent 3caa683626
commit a5daaee3ed
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -29,11 +29,11 @@ def notFollowedByRedefinedTermToken := notFollowedBy ("if" <|> "match" <|> "let"
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doId := parser! «try» (ident >> optType >> leftArrow) >> termParser
def doPat := parser! «try» (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
@[builtinDoElemParser] def doLetArrow := parser! "let " >> (doId <|> doPat)
def doIdDecl := parser! «try» (ident >> optType >> leftArrow) >> termParser
def doPatDecl := parser! «try» (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
@[builtinDoElemParser] def doLetArrow := parser! "let " >> (doIdDecl <|> doPatDecl)
@[builtinDoElemParser] def doReassign := parser! notFollowedByRedefinedTermToken >> (letIdDecl <|> letPatDecl)
@[builtinDoElemParser] def doReassignArrow := parser! notFollowedByRedefinedTermToken >> (doId <|> doPat)
@[builtinDoElemParser] def doReassignArrow := parser! notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
@[builtinDoElemParser] def doHave := parser! "have " >> Term.haveDecl
/-
In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as
@ -66,7 +66,7 @@ else if c_2 then
-/
@[builtinDoElemParser] def doIf := parser! withPosition $
"if " >> optIdent >> termParser >> " then " >> doSeq
>> many (checkColGe "'else if' in 'do' must be indented" >> «try» (" else " >> " if ") >> optIdent >> termParser >> " then " >> doSeq)
>> many (checkColGe "'else if' in 'do' must be indented" >> group («try» (group (" else " >> " if ")) >> optIdent >> termParser >> " then " >> doSeq))
>> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
@[builtinDoElemParser] def doUnless := parser! "unless " >> withPosition (termParser >> optional ",") >> doSeq
@[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> withPosition (termParser >> optional ", ") >> doSeq