Documentation

Std.Classes.Cast

class NatCast (R : Type u) :
  • natCast : NatR

    The canonical map Nat → R.

Type class for the canonical homomorphism Nat → R.

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

    Instances For
      instance instCoeTailNat {R : Type u_1} [NatCast R] :
      instance instCoeHTCTNat {R : Type u_1} [NatCast R] :

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

      class IntCast (R : Type u) :
      • intCast : IntR

        The canonical map Int → R.

      Type class for the canonical homomorphism Int → R.

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

        Instances For
          instance instCoeTailInt {R : Type u_1} [IntCast R] :
          instance instCoeHTCTInt {R : Type u_1} [IntCast R] :