commit: c27474341e55a1a3432662273ef7bd1b9aa9231a

[log]
author: Scott Morrison <scott.morrison@gmail.com>

Tue Feb 13 15:47:11 2024 +1100
committer: GitHub <noreply@github.com>

Tue Feb 13 04:47:11 2024 +0000
tree: f6d585f5464f9cb44ae71417767ce17cfb27e5bc
parent: 27b962f14d96f34f6d6e905cc8a317d73ca6c8b2 [diff]

chore: upstream change tactic (#3308)

We previously had the syntax for `change` and `change at`, but no
implementation.

This moves Kyle's implementation from Std.

This also changes the `changeLocalDecl` function to push nodes to the
infotree about FVar aliases.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Lean/Elab/Tactic.lean[diff]
src/Lean/Elab/Tactic/Change.lean[Added - diff]
src/Lean/Meta/Tactic/Replace.lean[diff]
tests/lean/run/change_tac.lean[Added - diff]

4 files changed

tree: f6d585f5464f9cb44ae71417767ce17cfb27e5bc

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.