commit: 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387

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

Sun Jan 26 17:31:25 2025 -0800
committer: GitHub <noreply@github.com>

Mon Jan 27 01:31:25 2025 +0000
tree: fae6e14961d8d3b423055e3efd42666dc2ca8af5
parent: 98bd162ad46bdcb9bb63e7c77f70fc98cd9851eb [diff]

feat: `grind?` infrastructure  (#6785)

This PR adds infrastructure for the `grind?` tactic. It also adds the
new modifier `usr` which allows users to write `grind only [usr
thmName]` to instruct `grind` to only use theorem `thmName`, but using
the patterns specified with the command `grind_pattern`.

5 files changed

tree: fae6e14961d8d3b423055e3efd42666dc2ca8af5

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).