commit: 771a3e668f6f0892c5bfd91f78e4dac03c5be801

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

Mon Oct 20 17:13:32 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Oct 20 17:15:27 2025 -0700
tree: cf814ad6b768bd380c9f1e00c9aed0e94fb51831
parent: e3a5369bd7705e732d571319a7d3513ba9a70a63 [diff]

feat: improve `done` tactic in `grind` interactive mode

This PR improves the `done` tactic in `grind` interactive mode. It now
displays the `grind` state diagnostics for all unsolved subgoals.

2 files changed

tree: cf814ad6b768bd380c9f1e00c9aed0e94fb51831

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.