ink

class NatCast (R : Type u) : Type u

• The canonical map Nat → R→ R.

  natCast : Nat → R

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

ink

instance instNatCastNat : NatCast Nat

Equations

• instNatCastNat = { natCast := fun n => n }

ink

instance instNatCastInt : NatCast Int

Equations

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

ink

@[match_pattern]

def Nat.cast {R : Type u} [inst : 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

ink

instance instCoeTailNat {R : Type u_1} [inst : NatCast R] : CoeTail Nat R

Equations

• instCoeTailNat = { coe := Nat.cast }

ink

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

Equations

• instCoeHTCTNat = { coe := Nat.cast }

ink

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 }

ink

class IntCast (R : Type u) : Type u

• The canonical map Int → R→ R.

  intCast : Int → R

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

ink

instance instIntCastInt : IntCast Int

Equations

• instIntCastInt = { intCast := fun n => n }

ink

@[match_pattern]

def Int.cast {R : Type u} [inst : 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

ink

instance instCoeTailInt {R : Type u_1} [inst : IntCast R] : CoeTail Int R

Equations

• instCoeTailInt = { coe := Int.cast }

ink

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

Equations

• instCoeHTCTInt = { coe := Int.cast }