Skip to content

Commit

Permalink
perf: remove unnecessary, cache-defeating withPosition in `doReassi…
Browse files Browse the repository at this point in the history
…gnArrow`
  • Loading branch information
Kha authored and leodemoura committed Nov 28, 2022
1 parent 9dbd9ec commit 0795306
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Parser/Do.lean
Expand Up @@ -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
/-
Expand Down

0 comments on commit 0795306

Please sign in to comment.