Documentation

Std.Classes.Cast

class NatCast (R : Type u) :

Type class for the canonical homomorphism Nat → R.

  • natCast : NatR

    The canonical map Nat → R.

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

      Type class for the canonical homomorphism Int → R.

      • intCast : IntR

        The canonical map Int → R.

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