commit: a912652b7ddb9818bac123956ff8e2f8af4a3c83

[log]
author: Rob23oba <152706811+Rob23oba@users.noreply.github.com>

Tue May 27 09:07:12 2025 +0200
committer: GitHub <noreply@github.com>

Tue May 27 07:07:12 2025 +0000
tree: 45482897fcfe6c830b140237cc1c29abdfa7bde9
parent: 3af9ab64ed79a667fb8989f7a0c258b018aba371 [diff]

fix: `simp_all?` and `simp_all?!` (#8491)

This PR fixes the behavior of `simp_all?` and `simp_all?!`, aligning
them with `simp_all` and `simp_all!` respectively.

Closes #8490

src/Lean/Elab/Tactic/SimpTrace.lean[diff]
tests/lean/run/issue8490.lean[Added - diff]

2 files changed

tree: 45482897fcfe6c830b140237cc1c29abdfa7bde9

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.