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

fix(library/init/lean/parser/parser): bug

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-01 17:15:12 -07:00
parent 7361dc7b96
commit 6672cc2a34
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/parser/parser.lean
View file

@ -366,7 +366,7 @@ def many1 (p : parser α) : parser (list α) :=
do r ← remaining, many1_aux p r
def many (p : parser α) : parser (list α) :=
many1 p <* eps
many1 p <|> return []
def many1_aux' (p : parser α) : nat → parser unit
| 0 := p >> return ()
@ -376,7 +376,7 @@ def many1' (p : parser α) : parser unit :=
do r ← remaining, many1_aux' p r
def many' (p : parser α) : parser unit :=
many1' p <* eps
many1' p <|> return ()
def eoi : parser unit :=
λ it, if it.remaining = 0 then ok_eps () it { pos := it.offset }