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

chore: remove leftover

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-26 16:10:29 -07:00
parent 6892a957d6
commit ee4dc452ac
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -78,9 +78,7 @@ withPosition fun pos₁ =>
("; "
-- check indentation
>> checkColGe pos₁.column "do-elements must be indented"
-- no black lines between do-elements.
-- >> checkLineLe (pos₂.line+1) "no blank lines between do-elements"
>> notFollowedByCommandToken)
>> notFollowedByCommandToken)
>> optional (try ("; " >> notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)))
def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent