commit: 3b59c5c51ac70280f5e7b28fe2dc6029695c0478

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

Fri Feb 13 16:28:03 2026 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Fri Feb 13 16:28:03 2026 -0800
tree: db636e100c047b0d5614d22f566953293e78ae5f
parent: 6ca23a7b8bee57152110ce500ce795148707d4ed [diff]

fix: assertion violation in `mkEqProofImpl`

This PR fixes an assertion violation in `grind` reported at #12246
This assertion fails when in examples containing heterogenous
equalities with elements of different types (e.g., `Fin n` and `Fin m`) attached to the same
theory solver.

Closes #12246

3 files changed

tree: db636e100c047b0d5614d22f566953293e78ae5f

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.