From ae0d4e3ac4257edfe752dd9efdb202f5c93e5e57 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 22 Mar 2026 08:25:21 -0700 Subject: [PATCH] chore: remove `change ... with` tactic syntax (#13029) This PR removes the unused `change ... with` tactic syntax. It's been asked about a number of times recently, but it was never implemented. In PR #6018 we decided it was a Lean-3-ism. --- src/Init/Tactics.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 424809d532..dccfd26d8f 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -524,9 +524,6 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp) -/ syntax (name := change) "change " term (location)? : tactic -@[tactic_alt change] -syntax (name := changeWith) "change " term " with " term (location)? : tactic - /-- `show t` finds the first goal whose target unifies with `t`. It makes that the main goal, performs the unification, and replaces the target with the unified version of `t`.