commit: 32adce928c8376d7f6d8ab51c61bd2dc378d2c0c

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

Sat Dec 28 16:24:52 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Dec 28 16:27:26 2024 -0800
tree: 6862504b78aac0a2bd1dadb38d19efc3f5483ba3
parent: 5930db946cd91bbdf8115c4ce06173d27530fe5c [diff]

feat: add `grind_pattern` command

This PR introduces a command for specifying patterns used in the
heuristic instantiation of global theorems in the `grind` tactic.
Note that this PR only adds the parser.

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

2 files changed

tree: 6862504b78aac0a2bd1dadb38d19efc3f5483ba3

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 (documentation source: doc/make/index.md).