Kim Morrison cc493e688b feat: embed a NatModule in its IntModule completion (#8963) ... This PR embeds a NatModule into its IntModule completion, which is injective when we have AddLeftCancel, and monotone when the modules are ordered. Also adds some (failing) grind test cases that can be verified once `grind` uses this embedding.		2025-06-24 05:30:43 +00:00
..
bench	chore: add .dSYM files (Mac debug symbols) to tests .gitignore files (#8771)	2025-06-13 15:27:46 +00:00
compiler	fix: avoid caching uses of never_extract constants in toLCNF (#8956)	2025-06-24 02:04:56 +00:00
elabissues
ir
lean	feat: embed a NatModule in its IntModule completion (#8963)	2025-06-24 05:30:43 +00:00
pkg	feat: server support for new module setup (#8699)	2025-06-23 18:00:14 +00:00
playground
plugin	chore: add .dSYM files (Mac debug symbols) to tests .gitignore files (#8771)	2025-06-13 15:27:46 +00:00
simpperf
.gitignore
common.sh
lakefile.toml	chore: allow module in tests (#8881)	2025-06-21 02:49:22 +00:00
lean-toolchain