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

fix(library/init/lean/parser/parser): typo startPart ==> startPos

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-16 09:36:44 -07:00
parent 0c4708ad28
commit 260ea04add
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

@ -726,7 +726,7 @@ match tk with
def mkIdResult (startPos : Nat) (tk : Option TokenConfig) (val : Name) : BasicParserFn :=
fun c s =>
let stopPos := s.pos;
let stopPos := s.pos;
if isToken startPos stopPos tk then
mkTokenAndFixPos startPos tk c s
else
@ -769,7 +769,7 @@ partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → Bas
let s := s.next input s.pos;
identFnAux r c s
else
mkIdResult startPart tk r c s
mkIdResult startPos tk r c s
else
mkTokenAndFixPos startPos tk c s