commit: 6c6181e2d8ecedb89dcd9af066f5f54535a11e03

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

Wed Aug 06 13:22:15 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Aug 06 13:50:34 2025 -0700
tree: f48b65e1de9b164532454368688977acdfd5ae1a
parent: e332adf3d51c3be0cc1ce96ac4f55a1012cbe012 [diff]

fix: projection propagation in `grind`

This PR fixes a bug in the projection over constructor propagator used
in `grind`. It may construct type incorrect terms when a equivalence
class contains heterogeneous equalities.

closes #9769

src/Lean/Meta/Tactic/Grind/Proj.lean[diff]
tests/lean/run/grind_9769.lean[Added - diff]

2 files changed

tree: f48b65e1de9b164532454368688977acdfd5ae1a

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.