Leonardo de Moura 7034310a3b fix: disequality proof construction in grind (#9578) ... This PR fixes an issue in `grind`'s disequality proof construction. The issue occurs when an equality is merged with the `False` equivalence class, but it is not the root of its congruence class, and its congruence root has not yet been merged into the `False` equivalence class yet. closes #9562		2025-07-27 14:49:10 +00:00
..
bench	chore: add grind tests as benchmarks (#9537)	2025-07-25 14:21:38 +00:00
compiler
elabissues
ir
lean	fix: disequality proof construction in grind (#9578)	2025-07-27 14:49:10 +00:00
pkg	refactor: module-ize Lean (#9330)	2025-07-25 12:02:51 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain