commit: ee03c5f3657959a8c99a64c674f63c11899c5c85

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

Sat Nov 15 11:14:17 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Nov 15 12:10:11 2025 -0800
tree: b6b0c43d1480515db87701559421b0eb31d2cb0e
parent: f4cd97ce04f66d422616b82cd50d562a1fc80d00 [diff]

fix: incorrect `grind` param warning

This PR the redundant `grind` parameter warning message. It now checks
the `grind` theorem instantiation constraints too.

3 files changed

tree: b6b0c43d1480515db87701559421b0eb31d2cb0e

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.