chore: remove upstreamed Coe* Nat instances

* see: mathlib4#2878, std4#107
leanprover-community · Mar 17, 2023 · 37fc027 · 37fc027
1 parent b70bb6e
commit 37fc027
Showing 1 changed file with 0 additions and 9 deletions.
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -39,15 +39,6 @@ protected def Nat.unaryCast {R : Type u} [One R] [Zero R] [Add R] : ℕ → R
 
 #align nat.cast Nat.cast
 
--- see note [coercion into rings]
-instance [NatCast R] : CoeTail ℕ R where coe := Nat.cast
-
--- see note [coercion into rings]
-instance [NatCast R] : CoeHTCT ℕ R where coe := Nat.cast
-
-/-- This instance is needed to ensure that `instCoeNatInt` is not used. -/
-instance : Coe ℕ ℤ where coe := Nat.cast
-
 -- the following four declarations are not in mathlib3 and are relevant to the way numeric
 -- literals are handled in Lean 4.