# Documentation

Std.Classes.Cast

class NatCast (R : Type u) :
• The canonical map Nat → R→ R.

natCast : NatR

Type class for the canonical homomorphism Nat → R→ R.

Instances
instance instNatCastNat :
Equations
instance instNatCastInt :
Equations
@[match_pattern]
def Nat.cast {R : Type u} [inst : ] :
NatR

Canonical homomorphism from Nat to a additive monoid R with a 1. This is just the bare function in order to aid in creating instances of AddMonoidWithOne.

Equations
• Nat.cast = NatCast.natCast
instance instCoeTailNat {R : Type u_1} [inst : ] :
Equations
• instCoeTailNat = { coe := Nat.cast }
instance instCoeHTCTNat {R : Type u_1} [inst : ] :
Equations
• instCoeHTCTNat = { coe := Nat.cast }
instance instCoeNatInt_1 :

This instance is needed to ensure that instCoeNatInt from core is not used.

Equations
class IntCast (R : Type u) :
• The canonical map Int → R→ R.

intCast : IntR

Type class for the canonical homomorphism Int → R→ R.

Instances
instance instIntCastInt :
Equations
@[match_pattern]
def Int.cast {R : Type u} [inst : ] :
IntR

Canonical homomorphism from Int to a additive group R with a 1. This is just the bare function in order to aid in creating instances of AddGroupWithOne.

Equations
• Int.cast = IntCast.intCast
instance instCoeTailInt {R : Type u_1} [inst : ] :
Equations
• instCoeTailInt = { coe := Int.cast }
instance instCoeHTCTInt {R : Type u_1} [inst : ] :
Equations
• instCoeHTCTInt = { coe := Int.cast }