From 07953062ed590e58612bc0f85471cd926e7a33d4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 14 Nov 2022 13:34:24 +0100 Subject: [PATCH] perf: remove unnecessary, cache-defeating `withPosition` in `doReassignArrow` --- src/Lean/Parser/Do.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 6a72c625d5..246d528f2d 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -70,7 +70,7 @@ def letIdDeclNoBinders := node ``letIdDecl <| @[builtin_doElem_parser] def doReassign := leading_parser notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl) @[builtin_doElem_parser] def doReassignArrow := leading_parser - notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl) + notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl) @[builtin_doElem_parser] def doHave := leading_parser "have " >> Term.haveDecl /-