From 260ea04add4d7362927508d0ea246a7b6492eb39 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jul 2019 09:36:44 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): typo `startPart` ==> `startPos` --- library/init/lean/parser/parser.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 23a8129481..09a5fcbbb3 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -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