commit: ec7add0b48dee49255a9ac6ec3324ee81aaaebdd

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

Sat Sep 20 01:06:05 2025 -0700
committer: GitHub <noreply@github.com>

Sat Sep 20 08:06:05 2025 +0000
tree: 1250c00c83c110352fe96ed7f522d0a9b7370fd3
parent: 9b842b7554b932f51bd7efe4e76791dd596025ed [diff]

doc: `!` modifier in `grind` parameters (#10474)

This PR adds a doc string for the `!` parameter modifier in `grind`.

src/Init/Grind/Tactics.lean[diff]

1 file changed

tree: 1250c00c83c110352fe96ed7f522d0a9b7370fd3

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.