Documentation

Init.Data.UInt.Basic

@[extern lean_uint8_of_nat]
def UInt8.ofNat (n : Nat) :
Equations
Instances For
    @[inline, reducible]
    abbrev Nat.toUInt8 (n : Nat) :
    Equations
    Instances For
      @[extern lean_uint8_to_nat]
      def UInt8.toNat (n : UInt8) :
      Equations
      Instances For
        @[extern lean_uint8_add]
        def UInt8.add (a : UInt8) (b : UInt8) :
        Equations
        Instances For
          @[extern lean_uint8_sub]
          def UInt8.sub (a : UInt8) (b : UInt8) :
          Equations
          Instances For
            @[extern lean_uint8_mul]
            def UInt8.mul (a : UInt8) (b : UInt8) :
            Equations
            Instances For
              @[extern lean_uint8_div]
              def UInt8.div (a : UInt8) (b : UInt8) :
              Equations
              Instances For
                @[extern lean_uint8_mod]
                def UInt8.mod (a : UInt8) (b : UInt8) :
                Equations
                Instances For
                  @[extern lean_uint8_modn]
                  def UInt8.modn (a : UInt8) (n : Nat) :
                  Equations
                  Instances For
                    @[extern lean_uint8_land]
                    def UInt8.land (a : UInt8) (b : UInt8) :
                    Equations
                    Instances For
                      @[extern lean_uint8_lor]
                      def UInt8.lor (a : UInt8) (b : UInt8) :
                      Equations
                      Instances For
                        @[extern lean_uint8_xor]
                        def UInt8.xor (a : UInt8) (b : UInt8) :
                        Equations
                        Instances For
                          @[extern lean_uint8_shift_left]
                          def UInt8.shiftLeft (a : UInt8) (b : UInt8) :
                          Equations
                          Instances For
                            @[extern lean_uint8_shift_right]
                            Equations
                            Instances For
                              def UInt8.lt (a : UInt8) (b : UInt8) :
                              Equations
                              Instances For
                                def UInt8.le (a : UInt8) (b : UInt8) :
                                Equations
                                Instances For
                                  instance instOfNatUInt8 {n : Nat} :
                                  Equations
                                  Equations
                                  Equations
                                  Equations
                                  Equations
                                  Equations
                                  instance instLTUInt8 :
                                  Equations
                                  instance instLEUInt8 :
                                  Equations
                                  @[extern lean_uint8_complement]
                                  Equations
                                  Instances For
                                    Equations
                                    @[extern lean_uint8_dec_lt]
                                    def UInt8.decLt (a : UInt8) (b : UInt8) :
                                    Decidable (a < b)
                                    Equations
                                    Instances For
                                      @[extern lean_uint8_dec_le]
                                      def UInt8.decLe (a : UInt8) (b : UInt8) :
                                      Equations
                                      Instances For
                                        Equations
                                        Equations
                                        @[extern lean_uint16_of_nat]
                                        Equations
                                        Instances For
                                          @[inline, reducible]
                                          abbrev Nat.toUInt16 (n : Nat) :
                                          Equations
                                          Instances For
                                            @[extern lean_uint16_to_nat]
                                            Equations
                                            Instances For
                                              @[extern lean_uint16_add]
                                              def UInt16.add (a : UInt16) (b : UInt16) :
                                              Equations
                                              Instances For
                                                @[extern lean_uint16_sub]
                                                def UInt16.sub (a : UInt16) (b : UInt16) :
                                                Equations
                                                Instances For
                                                  @[extern lean_uint16_mul]
                                                  def UInt16.mul (a : UInt16) (b : UInt16) :
                                                  Equations
                                                  Instances For
                                                    @[extern lean_uint16_div]
                                                    def UInt16.div (a : UInt16) (b : UInt16) :
                                                    Equations
                                                    Instances For
                                                      @[extern lean_uint16_mod]
                                                      def UInt16.mod (a : UInt16) (b : UInt16) :
                                                      Equations
                                                      Instances For
                                                        @[extern lean_uint16_modn]
                                                        def UInt16.modn (a : UInt16) (n : Nat) :
                                                        Equations
                                                        Instances For
                                                          @[extern lean_uint16_land]
                                                          def UInt16.land (a : UInt16) (b : UInt16) :
                                                          Equations
                                                          Instances For
                                                            @[extern lean_uint16_lor]
                                                            def UInt16.lor (a : UInt16) (b : UInt16) :
                                                            Equations
                                                            Instances For
                                                              @[extern lean_uint16_xor]
                                                              def UInt16.xor (a : UInt16) (b : UInt16) :
                                                              Equations
                                                              Instances For
                                                                @[extern lean_uint16_shift_left]
                                                                Equations
                                                                Instances For
                                                                  @[extern lean_uint16_to_uint8]
                                                                  Equations
                                                                  Instances For
                                                                    @[extern lean_uint8_to_uint16]
                                                                    Equations
                                                                    Instances For
                                                                      @[extern lean_uint16_shift_right]
                                                                      Equations
                                                                      Instances For
                                                                        def UInt16.lt (a : UInt16) (b : UInt16) :
                                                                        Equations
                                                                        Instances For
                                                                          def UInt16.le (a : UInt16) (b : UInt16) :
                                                                          Equations
                                                                          Instances For
                                                                            instance instOfNatUInt16 {n : Nat} :
                                                                            Equations
                                                                            Equations
                                                                            Equations
                                                                            @[extern lean_uint16_complement]
                                                                            Equations
                                                                            Instances For
                                                                              @[extern lean_uint16_dec_lt]
                                                                              def UInt16.decLt (a : UInt16) (b : UInt16) :
                                                                              Decidable (a < b)
                                                                              Equations
                                                                              Instances For
                                                                                @[extern lean_uint16_dec_le]
                                                                                def UInt16.decLe (a : UInt16) (b : UInt16) :
                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  Equations
                                                                                  @[extern lean_uint32_of_nat]
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[extern lean_uint32_of_nat]
                                                                                    def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) :
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline, reducible]
                                                                                      abbrev Nat.toUInt32 (n : Nat) :
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[extern lean_uint32_add]
                                                                                        def UInt32.add (a : UInt32) (b : UInt32) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[extern lean_uint32_sub]
                                                                                          def UInt32.sub (a : UInt32) (b : UInt32) :
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[extern lean_uint32_mul]
                                                                                            def UInt32.mul (a : UInt32) (b : UInt32) :
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[extern lean_uint32_div]
                                                                                              def UInt32.div (a : UInt32) (b : UInt32) :
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[extern lean_uint32_mod]
                                                                                                def UInt32.mod (a : UInt32) (b : UInt32) :
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[extern lean_uint32_modn]
                                                                                                  def UInt32.modn (a : UInt32) (n : Nat) :
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[extern lean_uint32_land]
                                                                                                    def UInt32.land (a : UInt32) (b : UInt32) :
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[extern lean_uint32_lor]
                                                                                                      def UInt32.lor (a : UInt32) (b : UInt32) :
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[extern lean_uint32_xor]
                                                                                                        def UInt32.xor (a : UInt32) (b : UInt32) :
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[extern lean_uint32_shift_left]
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[extern lean_uint32_shift_right]
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[extern lean_uint32_to_uint8]
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[extern lean_uint32_to_uint16]
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[extern lean_uint8_to_uint32]
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[extern lean_uint16_to_uint32]
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      instance instOfNatUInt32 {n : Nat} :
                                                                                                                      Equations
                                                                                                                      @[extern lean_uint32_complement]
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[extern lean_uint64_of_nat]
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[inline, reducible]
                                                                                                                          abbrev Nat.toUInt64 (n : Nat) :
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[extern lean_uint64_to_nat]
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[extern lean_uint64_add]
                                                                                                                              def UInt64.add (a : UInt64) (b : UInt64) :
                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[extern lean_uint64_sub]
                                                                                                                                def UInt64.sub (a : UInt64) (b : UInt64) :
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[extern lean_uint64_mul]
                                                                                                                                  def UInt64.mul (a : UInt64) (b : UInt64) :
                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    @[extern lean_uint64_div]
                                                                                                                                    def UInt64.div (a : UInt64) (b : UInt64) :
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      @[extern lean_uint64_mod]
                                                                                                                                      def UInt64.mod (a : UInt64) (b : UInt64) :
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[extern lean_uint64_modn]
                                                                                                                                        def UInt64.modn (a : UInt64) (n : Nat) :
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[extern lean_uint64_land]
                                                                                                                                          def UInt64.land (a : UInt64) (b : UInt64) :
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            @[extern lean_uint64_lor]
                                                                                                                                            def UInt64.lor (a : UInt64) (b : UInt64) :
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[extern lean_uint64_xor]
                                                                                                                                              def UInt64.xor (a : UInt64) (b : UInt64) :
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[extern lean_uint64_shift_left]
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[extern lean_uint64_shift_right]
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    def UInt64.lt (a : UInt64) (b : UInt64) :
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      def UInt64.le (a : UInt64) (b : UInt64) :
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[extern lean_uint64_to_uint8]
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[extern lean_uint64_to_uint16]
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[extern lean_uint64_to_uint32]
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[extern lean_uint8_to_uint64]
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                @[extern lean_uint16_to_uint64]
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[extern lean_uint32_to_uint64]
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    instance instOfNatUInt64 {n : Nat} :
                                                                                                                                                                    Equations
                                                                                                                                                                    Equations
                                                                                                                                                                    Equations
                                                                                                                                                                    @[extern lean_uint64_complement]
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[extern lean_bool_to_uint64]
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[extern lean_uint64_dec_lt]
                                                                                                                                                                        def UInt64.decLt (a : UInt64) (b : UInt64) :
                                                                                                                                                                        Decidable (a < b)
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[extern lean_uint64_dec_le]
                                                                                                                                                                          def UInt64.decLe (a : UInt64) (b : UInt64) :
                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                            Equations
                                                                                                                                                                            @[extern lean_usize_of_nat]
                                                                                                                                                                            def USize.ofNat (n : Nat) :
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline, reducible]
                                                                                                                                                                              abbrev Nat.toUSize (n : Nat) :
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[extern lean_usize_to_nat]
                                                                                                                                                                                def USize.toNat (n : USize) :
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[extern lean_usize_add]
                                                                                                                                                                                  def USize.add (a : USize) (b : USize) :
                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[extern lean_usize_sub]
                                                                                                                                                                                    def USize.sub (a : USize) (b : USize) :
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[extern lean_usize_mul]
                                                                                                                                                                                      def USize.mul (a : USize) (b : USize) :
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[extern lean_usize_div]
                                                                                                                                                                                        def USize.div (a : USize) (b : USize) :
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[extern lean_usize_mod]
                                                                                                                                                                                          def USize.mod (a : USize) (b : USize) :
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[extern lean_usize_modn]
                                                                                                                                                                                            def USize.modn (a : USize) (n : Nat) :
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[extern lean_usize_land]
                                                                                                                                                                                              def USize.land (a : USize) (b : USize) :
                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[extern lean_usize_lor]
                                                                                                                                                                                                def USize.lor (a : USize) (b : USize) :
                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[extern lean_usize_xor]
                                                                                                                                                                                                  def USize.xor (a : USize) (b : USize) :
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[extern lean_usize_shift_left]
                                                                                                                                                                                                    def USize.shiftLeft (a : USize) (b : USize) :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[extern lean_usize_shift_right]
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[extern lean_uint32_to_usize]
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[extern lean_usize_to_uint32]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            def USize.lt (a : USize) (b : USize) :
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def USize.le (a : USize) (b : USize) :
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                instance instOfNatUSize {n : Nat} :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                instance instLTUSize :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                instance instLEUSize :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                @[extern lean_usize_complement]
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  @[extern lean_usize_dec_lt]
                                                                                                                                                                                                                  def USize.decLt (a : USize) (b : USize) :
                                                                                                                                                                                                                  Decidable (a < b)
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[extern lean_usize_dec_le]
                                                                                                                                                                                                                    def USize.decLe (a : USize) (b : USize) :
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      theorem USize.modn_lt {m : Nat} (u : USize) :
                                                                                                                                                                                                                      m > 0USize.toNat (u % m) < m