Leonardo de Moura 06d6dbff5d feat: model-based theory combination in grind (#7641) ... This PR implements basic model-based theory combination in `grind`. `grind` can now solve examples such as ```lean example (f : Int → Int) (x : Int) : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by grind ```		2025-03-23 04:06:09 +00:00
..
bench	chore: more core proof benchmarks	2025-03-21 15:59:14 +01:00
compiler
elabissues
ir
lean	feat: model-based theory combination in grind (#7641)	2025-03-23 04:06:09 +00:00
pkg	feat: debug_assert! (#7256)	2025-03-03 16:34:44 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain