This library note got upstreamed to Batteries; we can delete it here.

Author: Vierkantor

Mathlib/Data/Nat/Cast/Defs.lean

@@ -71,22 +71,6 @@ class AddMonoidWithOne (R : Type*) extends NatCast R, AddMonoid R, One R where
 /-- An `AddCommMonoidWithOne` is an `AddMonoidWithOne` satisfying `a + b = b + a`. -/
 class AddCommMonoidWithOne (R : Type*) extends AddMonoidWithOne R, AddCommMonoid R
 
-library_note2 «coercion into rings»
-/--
-Coercions such as `Nat.castCoe` that go from a concrete structure such as
-`ℕ` to an arbitrary ring `R` should be set up as follows:
-```lean
-instance : CoeTail ℕ R where coe := ...
-instance : CoeHTCT ℕ R where coe := ...
-```
-
-It needs to be `CoeTail` instead of `Coe` because otherwise type-class
-inference would loop when constructing the transitive coercion `ℕ → ℕ → ℕ → ...`.
-Sometimes we also need to declare the `CoeHTCT` instance
-if we need to shadow another coercion
-(e.g. `Nat.cast` should be used over `Int.ofNat`).
--/
-
 namespace Nat
 
 variable [AddMonoidWithOne R]