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

chore: introduce doSeqItem kind

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-25 12:10:49 +01:00
parent bd7bb6f5b5
commit 375e6232e0
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -18,8 +18,9 @@ namespace Term
def leftArrow : Parser := unicodeSymbol " ← " " <- "
@[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
def doSeqIndent := parser! many1Indent $ group (ppLine >> doElemParser >> optional "; ")
def doSeqBracketed := parser! "{" >> withoutPosition (many1 (group (ppLine >> doElemParser >> optional "; "))) >> ppLine >> "}"
def doSeqItem := parser! ppLine >> doElemParser >> optional "; "
def doSeqIndent := parser! many1Indent doSeqItem
def doSeqBracketed := parser! "{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent
def notFollowedByRedefinedTermToken :=