class NatCast (R : Type u) : Type u

Type class for the canonical homomorphism Nat → R.

• natCast : Nat → R

  The canonical map Nat → R.

instance instNatCastNat : NatCast Nat

Equations

• instNatCastNat = { natCast := fun (n : Nat) => n }

instance instNatCastInt : NatCast Int

Equations

• instNatCastInt = { natCast := fun (n : Nat) => Int.ofNat n }

@[match_pattern, reducible]

def Nat.cast {R : Type u} [NatCast R] : Nat → R

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} [NatCast R] : CoeTail Nat R

Equations

• instCoeTailNat = { coe := Nat.cast }

instance instCoeHTCTNat {R : Type u_1} [NatCast R] : CoeHTCT Nat R

Equations

• instCoeHTCTNat = { coe := Nat.cast }

instance instCoeNatInt_1 : Coe Nat Int

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

Equations

• instCoeNatInt_1 = { coe := Nat.cast }

class IntCast (R : Type u) : Type u

Type class for the canonical homomorphism Int → R.

• intCast : Int → R

  The canonical map Int → R.

instance instIntCastInt : IntCast Int

Equations

• instIntCastInt = { intCast := fun (n : Int) => n }

@[match_pattern, reducible]

def Int.cast {R : Type u} [IntCast R] : Int → R

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} [IntCast R] : CoeTail Int R

Equations

• instCoeTailInt = { coe := Int.cast }

instance instCoeHTCTInt {R : Type u_1} [IntCast R] : CoeHTCT Int R

Equations

• instCoeHTCTInt = { coe := Int.cast }