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 =>