·
653 commits
to master
since this release
fix: remove global `NatCast (Fin n)` instance (#8620) This PR removes the `NatCast (Fin n)` global instance (both the direct instance, and the indirect one via `Lean.Grind.Semiring`), as that instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note however that in Mathlib this happens anyway!