max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove change ... with tactic syntax (#13029)

Browse source 
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.
This commit is contained in:
Kyle Miller 2026-03-22 08:25:21 -07:00 • committed by GitHub
parent 4bf7fa7447
commit ae0d4e3ac4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Tactics.lean
View file

@ -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`.