commit: c358b0c7341de7cdd732b8f09ab552f7405facfb

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

Mon Jan 05 18:55:02 2026 +1000
committer: GitHub <noreply@github.com>

Mon Jan 05 08:55:02 2026 +0000
tree: 12fb65f3227ea177f35e8f53b450d65da9bc1134
parent: 8207919728b9299f43b75e1efd52a6900580819b [diff]

feat: add guards for grind patterns for `getElem?_eq_none` theorems (#11761)

This PR adds some `grind_pattern` `guard` conditions to potentially
expensive theorems.

7 files changed

tree: 12fb65f3227ea177f35e8f53b450d65da9bc1134

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.