commit: 1981c626048bb5b9e8e519c67079dc9522530f49

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

Tue Oct 28 14:22:42 2025 +1100
committer: GitHub <noreply@github.com>

Tue Oct 28 03:22:42 2025 +0000
tree: 4bcd1dcf252ca24677d50e51ad5f3788bcfda477
parent: bb3dd13f729b163343ac06365d892dadfcab9528 [diff]

feat: make `grind +premises` more robust to bad suggestions (#10992)

This PR ensures that `grind +premises` silently drops warnings and
errors about bad suggestions.

2 files changed

tree: 4bcd1dcf252ca24677d50e51ad5f3788bcfda477

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.