commit: e99a30155b2fa244d0e606388ed1041b3bc894f6

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

Mon Feb 12 18:20:35 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Feb 12 18:29:14 2024 -0800
tree: 623244683789a08177466a323992e60dc6a8a797
parent: fbedb79b4694ef86162694b1b1b8c489ecbd71ac [diff]

fix: `simp` fails when custom discharger makes no progress

closes #2634

src/Lean/Elab/SyntheticMVars.lean[diff]
src/Lean/Elab/Tactic/Simp.lean[diff]
tests/lean/2634.lean[Added - diff]
tests/lean/2634.lean.expected.out[Added - diff]

4 files changed

tree: 623244683789a08177466a323992e60dc6a8a797

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.