commit: f4cd97ce04f66d422616b82cd50d562a1fc80d00

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

Sat Nov 15 11:08:03 2025 -0800
committer: GitHub <noreply@github.com>

Sat Nov 15 19:08:03 2025 +0000
tree: 311a2e6805a974261c8251e58b9144f669994313
parent: e39894e62d363322fa18af76e12e54799496e2c0 [diff]

feat: add `grind_pattern` constraint annotations (#11193)

This PR uses the new `grind_pattern` constraints to fix cases where an
unbounded number of theorem instantiations would be generated for
certain theorems in the standard library.

10 files changed

tree: 311a2e6805a974261c8251e58b9144f669994313

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.