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

chore: let rec in do blocks

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-01 10:40:11 -07:00
parent 94c7945bd3
commit 4e72530ce7
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -25,7 +25,8 @@ def doSeqIndent := many1Indent $ doElemParser >> optional "; "
def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
@[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)
@ -60,8 +61,8 @@ else if c_2 then
```
-/
@[builtinDoElemParser] def doIf := parser! withPosition $
"if " >> termParser >> " then " >> doSeq
>> many (checkColGe "'else if' in 'do' must be indented" >> «try» (" else " >> " if ") >> termParser >> " then " >> doSeq)
"if " >> optIdent >> termParser >> " then " >> doSeq
>> many (checkColGe "'else if' in 'do' must be indented" >> «try» (" else " >> " if ") >> optIdent >> termParser >> " then " >> doSeq)
>> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
@[builtinDoElemParser] def doUnless := parser! "unless " >> termParser >> "do " >> doSeq
@[builtinDoElemParser] def doFor := parser! "for " >> termParser >> " in " >> termParser >> "do " >> doSeq

4
src/Lean/Parser/Term.lean
View file

@ -162,9 +162,9 @@ def attrArg : Parser := ident <|> strLit <|> numLit
-- use `rawIdent` because of attribute names such as `instance`
def attrInstance := parser! rawIdent >> many attrArg
def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
def letRecDecls := sepBy1 (group (optional «attributes» >> letDecl)) ", "
@[builtinTermParser] def «letrec» :=
parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", ")
>> optional "; " >> termParser
parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optional "; " >> termParser
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser maxPrec
@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec