Documentation

Init.Grind.CommRing.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
instance UInt8.instNatCast :
NatCast UInt8
Equations
    source
    instance UInt8.instIntCast :
    IntCast UInt8
    Equations
      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
      instance UInt16.instNatCast :
      NatCast UInt16
      Equations
        source
        instance UInt16.instIntCast :
        IntCast UInt16
        Equations
          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
          instance UInt32.instNatCast :
          NatCast UInt32
          Equations
            source
            instance UInt32.instIntCast :
            IntCast UInt32
            Equations
              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
              instance UInt64.instNatCast :
              NatCast UInt64
              Equations
                source
                instance UInt64.instIntCast :
                IntCast UInt64
                Equations
                  source
                  theorem UInt64.intCast_ofNat (x : Nat) :
                  ↑(OfNat.ofNat x) = OfNat.ofNat x
                  source
                  instance USize.instNatCast :
                  NatCast USize
                  Equations
                    source
                    instance USize.instIntCast :
                    IntCast USize
                    Equations
                      source
                      theorem USize.intCast_ofNat (x : Nat) :
                      ↑(OfNat.ofNat x) = OfNat.ofNat x
                      source
                      instance Lean.Grind.instCommRingUInt8 :
                      CommRing UInt8
                      Equations
                        source
                        instance Lean.Grind.instIsCharPUInt8OfNatNat :
                        IsCharP UInt8 256
                        source
                        instance Lean.Grind.instCommRingUInt16 :
                        CommRing UInt16
                        Equations
                          source
                          instance Lean.Grind.instIsCharPUInt16OfNatNat :
                          IsCharP UInt16 65536
                          source
                          instance Lean.Grind.instCommRingUInt32 :
                          CommRing UInt32
                          Equations
                            source
                            instance Lean.Grind.instIsCharPUInt32OfNatNat :
                            IsCharP UInt32 4294967296
                            source
                            instance Lean.Grind.instCommRingUInt64 :
                            CommRing UInt64
                            Equations
                              source
                              instance Lean.Grind.instIsCharPUInt64OfNatNat :
                              IsCharP UInt64 18446744073709551616
                              source
                              instance Lean.Grind.instCommRingUSize :
                              CommRing USize
                              Equations
                                source
                                instance Lean.Grind.instIsCharPUSizeHPowNatOfNatNumBits :
                                IsCharP USize (2 ^ System.Platform.numBits)