commit: 2754679c6065d45d7a0e9746552eaf739947a4ca

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

Mon Sep 28 02:11:43 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Sep 28 02:11:43 2026 +0000
tree: ae2eaf61f3c9d308d9a0891340ba86cc7685555b
parent: 86941be18ef336b765f61e4faca3207342f70b96 [diff]

doc: explain the stop condition of the `[grind hom]` rewriter

This PR documents at `mkRewriter` when the homomorphism rewriter stops at an E-graph term, why no equality is lost, and which parent rules are skipped as a result.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

src/Lean/Meta/Tactic/Grind/Homomorphism.lean[diff]

1 file changed

tree: ae2eaf61f3c9d308d9a0891340ba86cc7685555b

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.