Leonardo de Moura 18cc1cec80 fix: grind instance normalization (#10179) ... This PR fixes `grind` instance normalization procedure. Some modules in grind use builtin instances defined directly in core (e.g., `cutsat`), while others synthesize them using `synthInstance` (e.g., `ring`). This inconsistency is problematic, as it may introduce mismatches and result in two different representations for the same term. This PR fixes the issue.		2025-08-30 02:24:26 +00:00
..
bench	chore: fix stdlib size benchmarks	2025-08-28 12:07:27 +02:00
compiler	fix: Unicode path support for Lean Windows executables (#10133)	2025-08-27 11:28:55 +00:00
elabissues
ir
lean	fix: grind instance normalization (#10179)	2025-08-30 02:24:26 +00:00
pkg	chore: improve error message on trying to access an identifier imported privately from the public scope (#10153)	2025-08-27 13:43:56 +00:00
playground	chore: eliminate uses of intros x y z (#9983)	2025-08-19 06:09:13 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain