Documentation

Init.Data.UInt.Basic

@[extern lean_uint8_of_nat]
def UInt8.ofNat (n : Nat) :
Equations
Instances For
    @[reducible, inline]
    abbrev Nat.toUInt8 (n : Nat) :
    Equations
    Instances For
      @[extern lean_uint8_to_nat]
      def UInt8.toNat (n : UInt8) :
      Equations
      • n.toNat = n.val
      Instances For
        @[extern lean_uint8_add]
        def UInt8.add (a : UInt8) (b : UInt8) :
        Equations
        • a.add b = { val := a.val + b.val }
        Instances For
          @[extern lean_uint8_sub]
          def UInt8.sub (a : UInt8) (b : UInt8) :
          Equations
          • a.sub b = { val := a.val - b.val }
          Instances For
            @[extern lean_uint8_mul]
            def UInt8.mul (a : UInt8) (b : UInt8) :
            Equations
            • a.mul b = { val := a.val * b.val }
            Instances For
              @[extern lean_uint8_div]
              def UInt8.div (a : UInt8) (b : UInt8) :
              Equations
              • a.div b = { val := a.val / b.val }
              Instances For
                @[extern lean_uint8_mod]
                def UInt8.mod (a : UInt8) (b : UInt8) :
                Equations
                • a.mod b = { val := a.val % b.val }
                Instances For
                  @[extern lean_uint8_modn]
                  def UInt8.modn (a : UInt8) (n : Nat) :
                  Equations
                  • a.modn n = { val := a.val.modn n }
                  Instances For
                    @[extern lean_uint8_land]
                    def UInt8.land (a : UInt8) (b : UInt8) :
                    Equations
                    • a.land b = { val := a.val.land b.val }
                    Instances For
                      @[extern lean_uint8_lor]
                      def UInt8.lor (a : UInt8) (b : UInt8) :
                      Equations
                      • a.lor b = { val := a.val.lor b.val }
                      Instances For
                        @[extern lean_uint8_xor]
                        def UInt8.xor (a : UInt8) (b : UInt8) :
                        Equations
                        • a.xor b = { val := a.val.xor b.val }
                        Instances For
                          @[extern lean_uint8_shift_left]
                          def UInt8.shiftLeft (a : UInt8) (b : UInt8) :
                          Equations
                          • a.shiftLeft b = { val := a.val <<< (b.modn 8).val }
                          Instances For
                            @[extern lean_uint8_shift_right]
                            Equations
                            • a.shiftRight b = { val := a.val >>> (b.modn 8).val }
                            Instances For
                              def UInt8.lt (a : UInt8) (b : UInt8) :
                              Equations
                              • a.lt b = (a.val < b.val)
                              Instances For
                                def UInt8.le (a : UInt8) (b : UInt8) :
                                Equations
                                • a.le b = (a.val b.val)
                                Instances For
                                  instance UInt8.instOfNat {n : Nat} :
                                  Equations
                                  Equations
                                  Equations
                                  Equations
                                  Equations
                                  Equations
                                  instance instLTUInt8 :
                                  Equations
                                  instance instLEUInt8 :
                                  Equations
                                  @[extern lean_uint8_complement]
                                  Equations
                                  • a.complement = 0 - (a + 1)
                                  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
                                        instance instDecidableLtUInt8 (a : UInt8) (b : UInt8) :
                                        Decidable (a < b)
                                        Equations
                                        instance instDecidableLeUInt8 (a : UInt8) (b : UInt8) :
                                        Equations
                                        Equations
                                        Equations
                                        @[extern lean_uint16_of_nat]
                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev Nat.toUInt16 (n : Nat) :
                                          Equations
                                          Instances For
                                            @[extern lean_uint16_to_nat]
                                            Equations
                                            • n.toNat = n.val
                                            Instances For
                                              @[extern lean_uint16_add]
                                              def UInt16.add (a : UInt16) (b : UInt16) :
                                              Equations
                                              • a.add b = { val := a.val + b.val }
                                              Instances For
                                                @[extern lean_uint16_sub]
                                                def UInt16.sub (a : UInt16) (b : UInt16) :
                                                Equations
                                                • a.sub b = { val := a.val - b.val }
                                                Instances For
                                                  @[extern lean_uint16_mul]
                                                  def UInt16.mul (a : UInt16) (b : UInt16) :
                                                  Equations
                                                  • a.mul b = { val := a.val * b.val }
                                                  Instances For
                                                    @[extern lean_uint16_div]
                                                    def UInt16.div (a : UInt16) (b : UInt16) :
                                                    Equations
                                                    • a.div b = { val := a.val / b.val }
                                                    Instances For
                                                      @[extern lean_uint16_mod]
                                                      def UInt16.mod (a : UInt16) (b : UInt16) :
                                                      Equations
                                                      • a.mod b = { val := a.val % b.val }
                                                      Instances For
                                                        @[extern lean_uint16_modn]
                                                        def UInt16.modn (a : UInt16) (n : Nat) :
                                                        Equations
                                                        • a.modn n = { val := a.val.modn n }
                                                        Instances For
                                                          @[extern lean_uint16_land]
                                                          def UInt16.land (a : UInt16) (b : UInt16) :
                                                          Equations
                                                          • a.land b = { val := a.val.land b.val }
                                                          Instances For
                                                            @[extern lean_uint16_lor]
                                                            def UInt16.lor (a : UInt16) (b : UInt16) :
                                                            Equations
                                                            • a.lor b = { val := a.val.lor b.val }
                                                            Instances For
                                                              @[extern lean_uint16_xor]
                                                              def UInt16.xor (a : UInt16) (b : UInt16) :
                                                              Equations
                                                              • a.xor b = { val := a.val.xor b.val }
                                                              Instances For
                                                                @[extern lean_uint16_shift_left]
                                                                Equations
                                                                • a.shiftLeft b = { val := a.val <<< (b.modn 16).val }
                                                                Instances For
                                                                  @[extern lean_uint16_to_uint8]
                                                                  Equations
                                                                  • a.toUInt8 = a.toNat.toUInt8
                                                                  Instances For
                                                                    @[extern lean_uint8_to_uint16]
                                                                    Equations
                                                                    • a.toUInt16 = { val := a.val, }
                                                                    Instances For
                                                                      @[extern lean_uint16_shift_right]
                                                                      Equations
                                                                      • a.shiftRight b = { val := a.val >>> (b.modn 16).val }
                                                                      Instances For
                                                                        def UInt16.lt (a : UInt16) (b : UInt16) :
                                                                        Equations
                                                                        • a.lt b = (a.val < b.val)
                                                                        Instances For
                                                                          def UInt16.le (a : UInt16) (b : UInt16) :
                                                                          Equations
                                                                          • a.le b = (a.val b.val)
                                                                          Instances For
                                                                            instance UInt16.instOfNat {n : Nat} :
                                                                            Equations
                                                                            Equations
                                                                            Equations
                                                                            @[extern lean_uint16_complement]
                                                                            Equations
                                                                            • a.complement = 0 - (a + 1)
                                                                            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
                                                                                  instance instDecidableLtUInt16 (a : UInt16) (b : UInt16) :
                                                                                  Decidable (a < b)
                                                                                  Equations
                                                                                  instance instDecidableLeUInt16 (a : UInt16) (b : UInt16) :
                                                                                  Equations
                                                                                  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

                                                                                      Converts the given natural number to UInt32, but returns 2^32 - 1 for natural numbers >= 2^32.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline]
                                                                                        abbrev Nat.toUInt32 (n : Nat) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[extern lean_uint32_add]
                                                                                          def UInt32.add (a : UInt32) (b : UInt32) :
                                                                                          Equations
                                                                                          • a.add b = { val := a.val + b.val }
                                                                                          Instances For
                                                                                            @[extern lean_uint32_sub]
                                                                                            def UInt32.sub (a : UInt32) (b : UInt32) :
                                                                                            Equations
                                                                                            • a.sub b = { val := a.val - b.val }
                                                                                            Instances For
                                                                                              @[extern lean_uint32_mul]
                                                                                              def UInt32.mul (a : UInt32) (b : UInt32) :
                                                                                              Equations
                                                                                              • a.mul b = { val := a.val * b.val }
                                                                                              Instances For
                                                                                                @[extern lean_uint32_div]
                                                                                                def UInt32.div (a : UInt32) (b : UInt32) :
                                                                                                Equations
                                                                                                • a.div b = { val := a.val / b.val }
                                                                                                Instances For
                                                                                                  @[extern lean_uint32_mod]
                                                                                                  def UInt32.mod (a : UInt32) (b : UInt32) :
                                                                                                  Equations
                                                                                                  • a.mod b = { val := a.val % b.val }
                                                                                                  Instances For
                                                                                                    @[extern lean_uint32_modn]
                                                                                                    def UInt32.modn (a : UInt32) (n : Nat) :
                                                                                                    Equations
                                                                                                    • a.modn n = { val := a.val.modn n }
                                                                                                    Instances For
                                                                                                      @[extern lean_uint32_land]
                                                                                                      def UInt32.land (a : UInt32) (b : UInt32) :
                                                                                                      Equations
                                                                                                      • a.land b = { val := a.val.land b.val }
                                                                                                      Instances For
                                                                                                        @[extern lean_uint32_lor]
                                                                                                        def UInt32.lor (a : UInt32) (b : UInt32) :
                                                                                                        Equations
                                                                                                        • a.lor b = { val := a.val.lor b.val }
                                                                                                        Instances For
                                                                                                          @[extern lean_uint32_xor]
                                                                                                          def UInt32.xor (a : UInt32) (b : UInt32) :
                                                                                                          Equations
                                                                                                          • a.xor b = { val := a.val.xor b.val }
                                                                                                          Instances For
                                                                                                            @[extern lean_uint32_shift_left]
                                                                                                            Equations
                                                                                                            • a.shiftLeft b = { val := a.val <<< (b.modn 32).val }
                                                                                                            Instances For
                                                                                                              @[extern lean_uint32_shift_right]
                                                                                                              Equations
                                                                                                              • a.shiftRight b = { val := a.val >>> (b.modn 32).val }
                                                                                                              Instances For
                                                                                                                @[extern lean_uint32_to_uint8]
                                                                                                                Equations
                                                                                                                • a.toUInt8 = a.toNat.toUInt8
                                                                                                                Instances For
                                                                                                                  @[extern lean_uint32_to_uint16]
                                                                                                                  Equations
                                                                                                                  • a.toUInt16 = a.toNat.toUInt16
                                                                                                                  Instances For
                                                                                                                    @[extern lean_uint8_to_uint32]
                                                                                                                    Equations
                                                                                                                    • a.toUInt32 = { val := a.val, }
                                                                                                                    Instances For
                                                                                                                      @[extern lean_uint16_to_uint32]
                                                                                                                      Equations
                                                                                                                      • a.toUInt32 = { val := a.val, }
                                                                                                                      Instances For
                                                                                                                        instance UInt32.instOfNat {n : Nat} :
                                                                                                                        Equations
                                                                                                                        @[extern lean_uint32_complement]
                                                                                                                        Equations
                                                                                                                        • a.complement = 0 - (a + 1)
                                                                                                                        Instances For
                                                                                                                          @[extern lean_uint64_of_nat]
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[reducible, inline]
                                                                                                                            abbrev Nat.toUInt64 (n : Nat) :
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[extern lean_uint64_to_nat]
                                                                                                                              Equations
                                                                                                                              • n.toNat = n.val
                                                                                                                              Instances For
                                                                                                                                @[extern lean_uint64_add]
                                                                                                                                def UInt64.add (a : UInt64) (b : UInt64) :
                                                                                                                                Equations
                                                                                                                                • a.add b = { val := a.val + b.val }
                                                                                                                                Instances For
                                                                                                                                  @[extern lean_uint64_sub]
                                                                                                                                  def UInt64.sub (a : UInt64) (b : UInt64) :
                                                                                                                                  Equations
                                                                                                                                  • a.sub b = { val := a.val - b.val }
                                                                                                                                  Instances For
                                                                                                                                    @[extern lean_uint64_mul]
                                                                                                                                    def UInt64.mul (a : UInt64) (b : UInt64) :
                                                                                                                                    Equations
                                                                                                                                    • a.mul b = { val := a.val * b.val }
                                                                                                                                    Instances For
                                                                                                                                      @[extern lean_uint64_div]
                                                                                                                                      def UInt64.div (a : UInt64) (b : UInt64) :
                                                                                                                                      Equations
                                                                                                                                      • a.div b = { val := a.val / b.val }
                                                                                                                                      Instances For
                                                                                                                                        @[extern lean_uint64_mod]
                                                                                                                                        def UInt64.mod (a : UInt64) (b : UInt64) :
                                                                                                                                        Equations
                                                                                                                                        • a.mod b = { val := a.val % b.val }
                                                                                                                                        Instances For
                                                                                                                                          @[extern lean_uint64_modn]
                                                                                                                                          def UInt64.modn (a : UInt64) (n : Nat) :
                                                                                                                                          Equations
                                                                                                                                          • a.modn n = { val := a.val.modn n }
                                                                                                                                          Instances For
                                                                                                                                            @[extern lean_uint64_land]
                                                                                                                                            def UInt64.land (a : UInt64) (b : UInt64) :
                                                                                                                                            Equations
                                                                                                                                            • a.land b = { val := a.val.land b.val }
                                                                                                                                            Instances For
                                                                                                                                              @[extern lean_uint64_lor]
                                                                                                                                              def UInt64.lor (a : UInt64) (b : UInt64) :
                                                                                                                                              Equations
                                                                                                                                              • a.lor b = { val := a.val.lor b.val }
                                                                                                                                              Instances For
                                                                                                                                                @[extern lean_uint64_xor]
                                                                                                                                                def UInt64.xor (a : UInt64) (b : UInt64) :
                                                                                                                                                Equations
                                                                                                                                                • a.xor b = { val := a.val.xor b.val }
                                                                                                                                                Instances For
                                                                                                                                                  @[extern lean_uint64_shift_left]
                                                                                                                                                  Equations
                                                                                                                                                  • a.shiftLeft b = { val := a.val <<< (b.modn 64).val }
                                                                                                                                                  Instances For
                                                                                                                                                    @[extern lean_uint64_shift_right]
                                                                                                                                                    Equations
                                                                                                                                                    • a.shiftRight b = { val := a.val >>> (b.modn 64).val }
                                                                                                                                                    Instances For
                                                                                                                                                      def UInt64.lt (a : UInt64) (b : UInt64) :
                                                                                                                                                      Equations
                                                                                                                                                      • a.lt b = (a.val < b.val)
                                                                                                                                                      Instances For
                                                                                                                                                        def UInt64.le (a : UInt64) (b : UInt64) :
                                                                                                                                                        Equations
                                                                                                                                                        • a.le b = (a.val b.val)
                                                                                                                                                        Instances For
                                                                                                                                                          @[extern lean_uint64_to_uint8]
                                                                                                                                                          Equations
                                                                                                                                                          • a.toUInt8 = a.toNat.toUInt8
                                                                                                                                                          Instances For
                                                                                                                                                            @[extern lean_uint64_to_uint16]
                                                                                                                                                            Equations
                                                                                                                                                            • a.toUInt16 = a.toNat.toUInt16
                                                                                                                                                            Instances For
                                                                                                                                                              @[extern lean_uint64_to_uint32]
                                                                                                                                                              Equations
                                                                                                                                                              • a.toUInt32 = a.toNat.toUInt32
                                                                                                                                                              Instances For
                                                                                                                                                                @[extern lean_uint8_to_uint64]
                                                                                                                                                                Equations
                                                                                                                                                                • a.toUInt64 = { val := a.val, }
                                                                                                                                                                Instances For
                                                                                                                                                                  @[extern lean_uint16_to_uint64]
                                                                                                                                                                  Equations
                                                                                                                                                                  • a.toUInt64 = { val := a.val, }
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[extern lean_uint32_to_uint64]
                                                                                                                                                                    Equations
                                                                                                                                                                    • a.toUInt64 = { val := a.val, }
                                                                                                                                                                    Instances For
                                                                                                                                                                      instance UInt64.instOfNat {n : Nat} :
                                                                                                                                                                      Equations
                                                                                                                                                                      Equations
                                                                                                                                                                      Equations
                                                                                                                                                                      @[extern lean_uint64_complement]
                                                                                                                                                                      Equations
                                                                                                                                                                      • a.complement = 0 - (a + 1)
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[extern lean_bool_to_uint64]
                                                                                                                                                                        Equations
                                                                                                                                                                        • b.toUInt64 = if b = true then 1 else 0
                                                                                                                                                                        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
                                                                                                                                                                              instance instDecidableLtUInt64 (a : UInt64) (b : UInt64) :
                                                                                                                                                                              Decidable (a < b)
                                                                                                                                                                              Equations
                                                                                                                                                                              instance instDecidableLeUInt64 (a : UInt64) (b : UInt64) :
                                                                                                                                                                              Equations
                                                                                                                                                                              Equations
                                                                                                                                                                              Equations
                                                                                                                                                                              @[deprecated]
                                                                                                                                                                              @[extern lean_usize_of_nat]
                                                                                                                                                                              def USize.ofNat (n : Nat) :
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                abbrev Nat.toUSize (n : Nat) :
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[extern lean_usize_to_nat]
                                                                                                                                                                                  def USize.toNat (n : USize) :
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • n.toNat = n.val
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[extern lean_usize_add]
                                                                                                                                                                                    def USize.add (a : USize) (b : USize) :
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • a.add b = { val := a.val + b.val }
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[extern lean_usize_sub]
                                                                                                                                                                                      def USize.sub (a : USize) (b : USize) :
                                                                                                                                                                                      Equations
                                                                                                                                                                                      • a.sub b = { val := a.val - b.val }
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[extern lean_usize_mul]
                                                                                                                                                                                        def USize.mul (a : USize) (b : USize) :
                                                                                                                                                                                        Equations
                                                                                                                                                                                        • a.mul b = { val := a.val * b.val }
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[extern lean_usize_div]
                                                                                                                                                                                          def USize.div (a : USize) (b : USize) :
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • a.div b = { val := a.val / b.val }
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[extern lean_usize_mod]
                                                                                                                                                                                            def USize.mod (a : USize) (b : USize) :
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • a.mod b = { val := a.val % b.val }
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[extern lean_usize_modn]
                                                                                                                                                                                              def USize.modn (a : USize) (n : Nat) :
                                                                                                                                                                                              Equations
                                                                                                                                                                                              • a.modn n = { val := a.val.modn n }
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[extern lean_usize_land]
                                                                                                                                                                                                def USize.land (a : USize) (b : USize) :
                                                                                                                                                                                                Equations
                                                                                                                                                                                                • a.land b = { val := a.val.land b.val }
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[extern lean_usize_lor]
                                                                                                                                                                                                  def USize.lor (a : USize) (b : USize) :
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • a.lor b = { val := a.val.lor b.val }
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[extern lean_usize_xor]
                                                                                                                                                                                                    def USize.xor (a : USize) (b : USize) :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • a.xor b = { val := a.val.xor b.val }
                                                                                                                                                                                                    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
                                                                                                                                                                                                            • a.toUInt32 = a.toNat.toUInt32
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def USize.lt (a : USize) (b : USize) :
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • a.lt b = (a.val < b.val)
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                def USize.le (a : USize) (b : USize) :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • a.le b = (a.val b.val)
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  instance USize.instOfNat {n : Nat} :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  instance instLTUSize :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  instance instLEUSize :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  @[extern lean_usize_complement]
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • a.complement = 0 - (a + 1)
                                                                                                                                                                                                                  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
                                                                                                                                                                                                                        instance instDecidableLtUSize (a : USize) (b : USize) :
                                                                                                                                                                                                                        Decidable (a < b)
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        instance instDecidableLeUSize (a : USize) (b : USize) :
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Equations