Documentation

Init.Grind.CommRing.SInt

source
instance Lean.Grind.instNatCastInt8 :
NatCast Int8
Equations
    source
    instance Lean.Grind.instIntCastInt8 :
    IntCast Int8
    Equations
      source
      instance Lean.Grind.instCommRingInt8 :
      CommRing Int8
      Equations
        source
        instance Lean.Grind.instIsCharPInt8HPowNatOfNat :
        IsCharP Int8 (2 ^ 8)
        source
        instance Lean.Grind.instNatCastInt16 :
        NatCast Int16
        Equations
          source
          instance Lean.Grind.instIntCastInt16 :
          IntCast Int16
          Equations
            source
            instance Lean.Grind.instCommRingInt16 :
            CommRing Int16
            Equations
              source
              instance Lean.Grind.instIsCharPInt16HPowNatOfNat :
              IsCharP Int16 (2 ^ 16)
              source
              instance Lean.Grind.instNatCastInt32 :
              NatCast Int32
              Equations
                source
                instance Lean.Grind.instIntCastInt32 :
                IntCast Int32
                Equations
                  source
                  instance Lean.Grind.instCommRingInt32 :
                  CommRing Int32
                  Equations
                    source
                    instance Lean.Grind.instIsCharPInt32HPowNatOfNat :
                    IsCharP Int32 (2 ^ 32)
                    source
                    instance Lean.Grind.instNatCastInt64 :
                    NatCast Int64
                    Equations
                      source
                      instance Lean.Grind.instIntCastInt64 :
                      IntCast Int64
                      Equations
                        source
                        instance Lean.Grind.instCommRingInt64 :
                        CommRing Int64
                        Equations
                          source
                          instance Lean.Grind.instIsCharPInt64HPowNatOfNat :
                          IsCharP Int64 (2 ^ 64)
                          source
                          instance Lean.Grind.instNatCastISize :
                          NatCast ISize
                          Equations
                            source
                            instance Lean.Grind.instIntCastISize :
                            IntCast ISize
                            Equations
                              source
                              instance Lean.Grind.instCommRingISize :
                              CommRing ISize
                              Equations
                                source
                                instance Lean.Grind.instIsCharPISizeHPowNatOfNatNumBits :
                                IsCharP ISize (2 ^ System.Platform.numBits)