commit: f8bce0eaaa8f2020330161bdf0e1b26348bf83d1

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

Sat Nov 29 16:50:30 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Nov 29 16:51:07 2025 -0800
tree: c6746303512393c2661e09a21d7bf731a45faaf3
parent: 075f1d66eb35aa3be8a0ce6df9deaaa900dafae8 [diff]

doc: add docstring for `grind_pattern` command

This PR documents the `grind_pattern` command for manually selecting
theorem instantiation patterns, including multi-patterns and the
constraint system (`=/=`, `=?=`, `size`, `depth`, `is_ground`,
`is_value`, `is_strict_value`, `gen`, `max_insts`, `guard`, `check`).

src/Lean/Meta/Tactic/Grind/Parser.lean[diff]

1 file changed

tree: c6746303512393c2661e09a21d7bf731a45faaf3

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.