commit: 08c3f3c2366db7000fd20267e84aeb6e06487323

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

Sat Aug 02 07:37:07 2025 +0200
committer: GitHub <noreply@github.com>

Sat Aug 02 05:37:07 2025 +0000
tree: 2cbcbbda6ac06358a0bf5a8468c6952bca0dfa6b
parent: a01eda79e8d930cbbea57253917011e3e9da6a07 [diff]

feat: warn `grind` redundant parameters (#9679)

This PR produces a warning for redundant `grind` arguments.

3 files changed

tree: 2cbcbbda6ac06358a0bf5a8468c6952bca0dfa6b

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.