commit: a8a160b09147c3225150703ac727eea6ee9a3b0e

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Sun Dec 15 01:56:57 2024 +0100
committer: GitHub <noreply@github.com>

Sun Dec 15 00:56:57 2024 +0000
tree: e6d0c64ddf0ae9902faf8e60da05b4a52796d056
parent: e08d35cea1893fac25c684036fead96b5ae47b10 [diff]

fix: `revertAll` must clear auxiliary declarations (#6386)

This PR ensures that `revertAll` clears auxiliary declarations when
invoked directly by users.

closes #6263

src/Lean/Meta/Tactic/Grind/RevertAll.lean[diff]
tests/lean/run/6263.lean[Added - diff]

2 files changed

tree: e6d0c64ddf0ae9902faf8e60da05b4a52796d056

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 (documentation source: doc/make/index.md).