Leonardo de Moura aa5b392e35 fix: canonicalization of non-standard OfNat.ofNat terms (#9481) ... This PR fixes a kernel type mismatch that occurs when using `grind` on goals containing non-standard `OfNat.ofNat` terms. For example, in issue #9477, the `0` in the theorem `range_lower` has the form: ```lean (@OfNat.ofNat (Std.PRange.Bound (Std.PRange.RangeShape.lower (Std.PRange.RangeShape.mk Std.PRange.BoundShape.closed Std.PRange.BoundShape.open)) Nat) (nat_lit 0) (instOfNatNat (nat_lit 0))) ``` instead of the more standard form: ```lean (@OfNat.ofNat Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) ``` Closes #9477		2025-07-23 04:10:21 +00:00
..
bench	chore: benchmark using USE_LAKE (#9361)	2025-07-17 18:44:29 +00:00
compiler
elabissues
ir
lean	fix: canonicalization of non-standard OfNat.ofNat terms (#9481)	2025-07-23 04:10:21 +00:00
pkg	perf: minimize exported codegen data (#9356)	2025-07-22 09:05:49 +00:00
playground	refactor: migrate all usages of old slice notation (#9000)	2025-06-27 18:52:07 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain