commit: a35d61e9e8333b60ac44312842dfa0a0a20e25f9

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

Sat Jul 26 13:18:38 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Jul 26 13:18:38 2025 -0700
tree: a6346f85a551ef97bd7983a530da08b6f012ed8b
parent: af84f76f318ef4af96611fce04dbc621f3c379ac [diff]

feat: add `grind` option `abstractProof`

This PR adds the option `abstractProof` to control whether `grind`
automatically creates an auxiliary theorem for the generated proof or not.

2 files changed

tree: a6346f85a551ef97bd7983a530da08b6f012ed8b

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.