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

fix: notFollowedBy info

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-26 11:44:53 -07:00
parent 45a98d5739
commit a1579f3123
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Basic.lean
View file

@ -498,8 +498,7 @@ fun c s =>
s.mkError "notFollowedBy"
@[inline] def notFollowedBy (p : Parser) : Parser :=
{ info := p.info,
fn := notFollowedByFn p.fn }
{ fn := notFollowedByFn p.fn }
@[specialize] partial def manyAux (p : ParserFn) : ParserFn
| c, s =>