commit: 4379002d0582ae96d7fc6ccf5921ff4e9aa7239e

[log]
author: Kim Morrison <477956+kim-em@users.noreply.github.com>

Thu Sep 18 16:29:53 2025 +1000
committer: GitHub <noreply@github.com>

Thu Sep 18 06:29:53 2025 +0000
tree: d0ebb6feda0f20e160d2e36dccd8f2c531a1fc25
parent: 5d50ec90f9fbcf15e6137cbc89458fe59870dea7 [diff]

feat: add `reprove` command for re-proving theorems with a specified tactic (#10434)

This PR adds `reprove N by T`, which effectively elaborates `example
type_of% N := by T`. It supports multiple identifiers. This is useful
for testing tactics.


🤖 Generated with [Claude Code](https://claude.ai/code)

---------

Co-authored-by: Claude <noreply@anthropic.com>

src/Lean/Util.lean[diff]
src/Lean/Util/Reprove.lean[Added - diff]
tests/lean/run/reprove.lean[Added - diff]

3 files changed

tree: d0ebb6feda0f20e160d2e36dccd8f2c531a1fc25

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.