Documentation

Init.GrindInstances.Ring.UInt

source
theorem UInt8.ofNat_mod_size' {x : Nat} :
ofNat (x % 256) = ofNat x

Variant of UInt8.ofNat_mod_size replacing 2 ^ 8 with 256.

source
@[implicit_reducible]
def UInt8.natCast :
NatCast UInt8
Instances For
    source
    @[implicit_reducible]
    def UInt8.intCast :
    IntCast UInt8
    Instances For
      source
      theorem UInt8.intCast_neg (x : Int) :
      ↑(-x) = -↑x
      source
      theorem UInt8.intCast_ofNat (x : Nat) :
      ↑(OfNat.ofNat x) = OfNat.ofNat x
      source
      theorem UInt16.ofNat_mod_size' {x : Nat} :
      ofNat (x % 65536) = ofNat x

      Variant of UInt16.ofNat_mod_size replacing 2 ^ 16 with 65536.

      source
      @[implicit_reducible]
      def UInt16.natCast :
      NatCast UInt16
      Instances For
        source
        @[implicit_reducible]
        def UInt16.intCast :
        IntCast UInt16
        Instances For
          source
          theorem UInt16.intCast_neg (x : Int) :
          ↑(-x) = -↑x
          source
          theorem UInt16.intCast_ofNat (x : Nat) :
          ↑(OfNat.ofNat x) = OfNat.ofNat x
          source
          theorem UInt32.ofNat_mod_size' {x : Nat} :
          ofNat (x % 4294967296) = ofNat x

          Variant of UInt32.ofNat_mod_size replacing 2 ^ 32 with 4294967296.

          source
          @[implicit_reducible]
          def UInt32.natCast :
          NatCast UInt32
          Instances For
            source
            @[implicit_reducible]
            def UInt32.intCast :
            IntCast UInt32
            Instances For
              source
              theorem UInt32.intCast_neg (x : Int) :
              ↑(-x) = -↑x
              source
              theorem UInt32.intCast_ofNat (x : Nat) :
              ↑(OfNat.ofNat x) = OfNat.ofNat x
              source
              theorem UInt64.ofNat_mod_size' {x : Nat} :
              ofNat (x % 18446744073709551616) = ofNat x

              Variant of UInt64.ofNat_mod_size replacing 2 ^ 64 with 18446744073709551616.

              source
              @[implicit_reducible]
              def UInt64.natCast :
              NatCast UInt64
              Instances For
                source
                @[implicit_reducible]
                def UInt64.intCast :
                IntCast UInt64
                Instances For
                  source
                  theorem UInt64.intCast_neg (x : Int) :
                  ↑(-x) = -↑x
                  source
                  theorem UInt64.intCast_ofNat (x : Nat) :
                  ↑(OfNat.ofNat x) = OfNat.ofNat x
                  source
                  @[implicit_reducible]
                  def USize.natCast :
                  NatCast USize
                  Instances For
                    source
                    @[implicit_reducible]
                    def USize.intCast :
                    IntCast USize
                    Instances For
                      source
                      theorem USize.intCast_neg (x : Int) :
                      ↑(-x) = -↑x
                      source
                      theorem USize.intCast_ofNat (x : Nat) :
                      ↑(OfNat.ofNat x) = OfNat.ofNat x
                      source
                      @[implicit_reducible]
                      instance Lean.Grind.instCommRingUInt8 :
                      CommRing UInt8
                      source
                      instance Lean.Grind.instIsCharPUInt8OfNatNat :
                      IsCharP UInt8 256
                      source
                      instance Lean.Grind.instPowUInt8UintOfNatNat :
                      ToInt.Pow UInt8 (IntInterval.uint 8)
                      source
                      @[implicit_reducible]
                      instance Lean.Grind.instCommRingUInt16 :
                      CommRing UInt16
                      source
                      instance Lean.Grind.instIsCharPUInt16OfNatNat :
                      IsCharP UInt16 65536
                      source
                      instance Lean.Grind.instPowUInt16UintOfNatNat :
                      ToInt.Pow UInt16 (IntInterval.uint 16)
                      source
                      @[implicit_reducible]
                      instance Lean.Grind.instCommRingUInt32 :
                      CommRing UInt32
                      source
                      instance Lean.Grind.instIsCharPUInt32OfNatNat :
                      IsCharP UInt32 4294967296
                      source
                      instance Lean.Grind.instPowUInt32UintOfNatNat :
                      ToInt.Pow UInt32 (IntInterval.uint 32)
                      source
                      @[implicit_reducible]
                      instance Lean.Grind.instCommRingUInt64 :
                      CommRing UInt64
                      source
                      instance Lean.Grind.instIsCharPUInt64OfNatNat :
                      IsCharP UInt64 18446744073709551616
                      source
                      instance Lean.Grind.instPowUInt64UintOfNatNat :
                      ToInt.Pow UInt64 (IntInterval.uint 64)
                      source
                      @[implicit_reducible]
                      instance Lean.Grind.instCommRingUSize :
                      CommRing USize
                      source
                      instance Lean.Grind.instIsCharPUSizeHPowNatOfNatNumBits :
                      IsCharP USize (2 ^ System.Platform.numBits)
                      source
                      instance Lean.Grind.instPowUSizeUintNumBits :
                      ToInt.Pow USize (IntInterval.uint System.Platform.numBits)