From 1636083caed52b3de12e5144a574c48d5fac4f4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Jul 2019 14:07:27 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): typo --- library/init/lean/parser/parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index a5a7d248e6..80a30d1459 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -646,7 +646,7 @@ match tk with | some tk => -- if a token is both a symbol and a valid identifier (i.e. a keyword), -- we want it to be recognized as a symbol - tk.val.bsize ≥ idStopPos - idStopPos + tk.val.bsize ≥ idStopPos - idStartPos def mkTokenAndFixPos (startPos : Nat) (tk : Option TokenConfig) : BasicParserFn := fun c s =>