commit: 3a733abe112d1093683ed5ded622457590a9c129

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

Thu Jan 02 10:47:53 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jan 02 10:51:56 2025 -0800
tree: 0245c18a516905ba37cf7873b7d8ceeec32b8eb1
parent: 3cba17140f85f1544b48e68941918c58244851cf [diff]

fix: congruence closure used in the `grind` tactic

This PR fixes a bug in the congruence closure data structure used in
the `grind` tactic. The new test includes an example that previously caused a
panic. A similar panic was also occurring in the test `grind_nested_proofs.lean`.

7 files changed

tree: 0245c18a516905ba37cf7873b7d8ceeec32b8eb1

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 (documentation source: doc/make/index.md).