class NatCast (R : Type u) : Type u

• natCast : Nat → R

  The canonical map Nat → R.

Type class for the canonical homomorphism Nat → R.

instance instNatCastNat : NatCast Nat

instance instNatCastInt : NatCast Int

@[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.

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

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

instance instCoeNatInt_1 : Coe Nat Int

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

class IntCast (R : Type u) : Type u

• intCast : Int → R

  The canonical map Int → R.

Type class for the canonical homomorphism Int → R.

instance instIntCastInt : IntCast Int

@[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.

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

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