commit: 0eaf79b48cfbfacbbcd2e26b2cbf8e1ffbeb4e02

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

Wed Oct 22 19:17:41 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Oct 22 19:25:16 2025 -0700
tree: 05cb2e0de133f9c4b5630e1787cf2902ef397007
parent: d748b0c8c95c56adfb3c7cb3e4907105355610c5 [diff]

feat: `grind` "silent" `have`

This PR implements the `have <ident>? : <prop>` tactic for the `grind`
interactive mode. The proposition is proved using the default `grind`
search strategy. This tactic is also useful for inspecting or querying the
current `grind` state.

5 files changed

tree: 05cb2e0de133f9c4b5630e1787cf2902ef397007

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.