Documentation

Init.GrindInstances.Ring.SInt

source
@[implicit_reducible]
def Lean.Grind.Int8.natCast :
NatCast Int8
Instances For
    source
    @[implicit_reducible]
    def Lean.Grind.Int8.intCast :
    IntCast Int8
    Instances For
      source
      theorem Lean.Grind.Int8.intCast_neg (i : Int) :
      ↑(-i) = -↑i
      source
      theorem Lean.Grind.Int8.intCast_ofNat (x : Nat) :
      ↑(OfNat.ofNat x) = OfNat.ofNat x
      source
      @[implicit_reducible]
      instance Lean.Grind.instCommRingInt8 :
      CommRing Int8
      source
      instance Lean.Grind.instIsCharPInt8HPowNatOfNat :
      IsCharP Int8 (2 ^ 8)
      source
      instance Lean.Grind.instPowInt8SintOfNatNat :
      ToInt.Pow Int8 (IntInterval.sint 8)
      source
      @[implicit_reducible]
      def Lean.Grind.Int16.natCast :
      NatCast Int16
      Instances For
        source
        @[implicit_reducible]
        def Lean.Grind.Int16.intCast :
        IntCast Int16
        Instances For
          source
          theorem Lean.Grind.Int16.intCast_neg (i : Int) :
          ↑(-i) = -↑i
          source
          theorem Lean.Grind.Int16.intCast_ofNat (x : Nat) :
          ↑(OfNat.ofNat x) = OfNat.ofNat x
          source
          @[implicit_reducible]
          instance Lean.Grind.instCommRingInt16 :
          CommRing Int16
          source
          instance Lean.Grind.instIsCharPInt16HPowNatOfNat :
          IsCharP Int16 (2 ^ 16)
          source
          instance Lean.Grind.instPowInt16SintOfNatNat :
          ToInt.Pow Int16 (IntInterval.sint 16)
          source
          @[implicit_reducible]
          def Lean.Grind.Int32.natCast :
          NatCast Int32
          Instances For
            source
            @[implicit_reducible]
            def Lean.Grind.Int32.intCast :
            IntCast Int32
            Instances For
              source
              theorem Lean.Grind.Int32.intCast_neg (i : Int) :
              ↑(-i) = -↑i
              source
              theorem Lean.Grind.Int32.intCast_ofNat (x : Nat) :
              ↑(OfNat.ofNat x) = OfNat.ofNat x
              source
              @[implicit_reducible]
              instance Lean.Grind.instCommRingInt32 :
              CommRing Int32
              source
              instance Lean.Grind.instIsCharPInt32HPowNatOfNat :
              IsCharP Int32 (2 ^ 32)
              source
              instance Lean.Grind.instPowInt32SintOfNatNat :
              ToInt.Pow Int32 (IntInterval.sint 32)
              source
              @[implicit_reducible]
              def Lean.Grind.Int64.natCast :
              NatCast Int64
              Instances For
                source
                @[implicit_reducible]
                def Lean.Grind.Int64.intCast :
                IntCast Int64
                Instances For
                  source
                  theorem Lean.Grind.Int64.intCast_neg (i : Int) :
                  ↑(-i) = -↑i
                  source
                  theorem Lean.Grind.Int64.intCast_ofNat (x : Nat) :
                  ↑(OfNat.ofNat x) = OfNat.ofNat x
                  source
                  @[implicit_reducible]
                  instance Lean.Grind.instCommRingInt64 :
                  CommRing Int64
                  source
                  instance Lean.Grind.instIsCharPInt64HPowNatOfNat :
                  IsCharP Int64 (2 ^ 64)
                  source
                  instance Lean.Grind.instPowInt64SintOfNatNat :
                  ToInt.Pow Int64 (IntInterval.sint 64)
                  source
                  @[implicit_reducible]
                  def Lean.Grind.ISize.natCast :
                  NatCast ISize
                  Instances For
                    source
                    @[implicit_reducible]
                    def Lean.Grind.ISize.intCast :
                    IntCast ISize
                    Instances For
                      source
                      theorem Lean.Grind.ISize.intCast_neg (i : Int) :
                      ↑(-i) = -↑i
                      source
                      theorem Lean.Grind.ISize.intCast_ofNat (x : Nat) :
                      ↑(OfNat.ofNat x) = OfNat.ofNat x
                      source
                      @[implicit_reducible]
                      instance Lean.Grind.instCommRingISize :
                      CommRing ISize
                      source
                      instance Lean.Grind.instIsCharPISizeHPowNatOfNatNumBits :
                      IsCharP ISize (2 ^ System.Platform.numBits)
                      source
                      instance Lean.Grind.instPowISizeSintNumBits :
                      ToInt.Pow ISize (IntInterval.sint System.Platform.numBits)