Documentation

Init.GrindInstances.Ring.SInt

source
def Lean.Grind.Int8.natCast :
NatCast Int8
Equations
    Instances For
      source
      def Lean.Grind.Int8.intCast :
      IntCast Int8
      Equations
        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
          instance Lean.Grind.instCommRingInt8 :
          CommRing Int8
          Equations
            source
            instance Lean.Grind.instIsCharPInt8HPowNatOfNat :
            IsCharP Int8 (2 ^ 8)
            source
            instance Lean.Grind.instPowInt8SintOfNatNat :
            ToInt.Pow Int8 (IntInterval.sint 8)
            source
            def Lean.Grind.Int16.natCast :
            NatCast Int16
            Equations
              Instances For
                source
                def Lean.Grind.Int16.intCast :
                IntCast Int16
                Equations
                  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
                    instance Lean.Grind.instCommRingInt16 :
                    CommRing Int16
                    Equations
                      source
                      instance Lean.Grind.instIsCharPInt16HPowNatOfNat :
                      IsCharP Int16 (2 ^ 16)
                      source
                      instance Lean.Grind.instPowInt16SintOfNatNat :
                      ToInt.Pow Int16 (IntInterval.sint 16)
                      source
                      def Lean.Grind.Int32.natCast :
                      NatCast Int32
                      Equations
                        Instances For
                          source
                          def Lean.Grind.Int32.intCast :
                          IntCast Int32
                          Equations
                            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
                              instance Lean.Grind.instCommRingInt32 :
                              CommRing Int32
                              Equations
                                source
                                instance Lean.Grind.instIsCharPInt32HPowNatOfNat :
                                IsCharP Int32 (2 ^ 32)
                                source
                                instance Lean.Grind.instPowInt32SintOfNatNat :
                                ToInt.Pow Int32 (IntInterval.sint 32)
                                source
                                def Lean.Grind.Int64.natCast :
                                NatCast Int64
                                Equations
                                  Instances For
                                    source
                                    def Lean.Grind.Int64.intCast :
                                    IntCast Int64
                                    Equations
                                      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
                                        instance Lean.Grind.instCommRingInt64 :
                                        CommRing Int64
                                        Equations
                                          source
                                          instance Lean.Grind.instIsCharPInt64HPowNatOfNat :
                                          IsCharP Int64 (2 ^ 64)
                                          source
                                          instance Lean.Grind.instPowInt64SintOfNatNat :
                                          ToInt.Pow Int64 (IntInterval.sint 64)
                                          source
                                          def Lean.Grind.ISize.natCast :
                                          NatCast ISize
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Grind.ISize.intCast :
                                              IntCast ISize
                                              Equations
                                                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
                                                  instance Lean.Grind.instCommRingISize :
                                                  CommRing ISize
                                                  Equations
                                                    source
                                                    instance Lean.Grind.instIsCharPISizeHPowNatOfNatNumBits :
                                                    IsCharP ISize (2 ^ System.Platform.numBits)
                                                    source
                                                    instance Lean.Grind.instPowISizeSintNumBits :
                                                    ToInt.Pow ISize (IntInterval.sint System.Platform.numBits)