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
    Equations
    Equations
    @[match_pattern]
    def Nat.cast {R : Type u} [inst : NatCast R] :
    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 : NatCast R] :
    Equations
    • instCoeTailNat = { coe := Nat.cast }
    instance instCoeHTCTNat {R : Type u_1} [inst : NatCast R] :
    Equations
    • instCoeHTCTNat = { coe := Nat.cast }

    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
      Equations
      @[match_pattern]
      def Int.cast {R : Type u} [inst : IntCast R] :
      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 : IntCast R] :
      Equations
      • instCoeTailInt = { coe := Int.cast }
      instance instCoeHTCTInt {R : Type u_1} [inst : IntCast R] :
      Equations
      • instCoeHTCTInt = { coe := Int.cast }