commit: 52e37e0d55e846bd74abbb52f394faffbf1f8b87

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

Tue Nov 04 18:34:17 2025 -0500
committer: GitHub <noreply@github.com>

Tue Nov 04 23:34:17 2025 +0000
tree: 46f3f533bf5148ef4410162c9dbd8fa56ff24060
parent: a4e073f5653f6ff11694c43695af009211df16b4 [diff]

refactor: `denote` functions in `grind` (#11071)

This PR ensures that the `denote` functions used to implement
proof-by-reflection terms in `grind` are abbreviations. This change
eliminates the need for the `withAbstractAtoms` gadget.

13 files changed

tree: 46f3f533bf5148ef4410162c9dbd8fa56ff24060

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.