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

fix: incorrect annotations

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-24 13:45:50 -07:00
parent 6343b97acb
commit e51b078015
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/Parsec.lean
View file

@ -69,7 +69,7 @@ def eof : Parsec Unit := fun it =>
else
success it ()
@[inline]
@[specialize]
partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
(do manyCore p (acc.push $ ←p))
<|> pure acc
@ -80,7 +80,7 @@ def many (p : Parsec α) : Parsec $ Array α := manyCore p #[]
@[inline]
def many1 (p : Parsec α) : Parsec $ Array α := do manyCore p #[←p]
@[inline]
@[specialize]
partial def manyCharsCore (p : Parsec Char) (acc : String) : Parsec String :=
(do manyCharsCore p (acc.push $ ←p))
<|> pure acc