Documentation

Init.Data.UInt.BasicAux

This module exists to provide the very basic UInt8 etc. definitions required for Init.Data.Char.Basic and Init.Data.Array.Basic. These are very important as they are used in meta code that is then (transitively) used in Init.Data.UInt.Basic and Init.Data.BitVec.Basic. This file thus breaks the import cycle that would be created by this dependency.

Converts a UInt8 into the corresponding Fin UInt8.size.

Equations
Instances For
    @[deprecated UInt8.toFin (since := "2025-02-12")]
    def UInt8.val (x : UInt8) :

    Converts a UInt8 into the corresponding Fin UInt8.size.

    Equations
    Instances For
      @[extern lean_uint8_of_nat]
      def UInt8.ofNat (n : Nat) :

      Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

      This function is overridden at runtime with an efficient implementation.

      Examples:

      Equations
      Instances For

        Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if the number is too large.

        Returns 2^8 - 1 for natural numbers greater than or equal to 2^8.

        Equations
        Instances For
          @[reducible, inline]
          abbrev Nat.toUInt8 (n : Nat) :

          Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

          This function is overridden at runtime with an efficient implementation.

          Examples:

          Equations
          Instances For
            @[extern lean_uint8_to_nat]
            def UInt8.toNat (n : UInt8) :

            Converts an 8-bit unsigned integer to an arbitrary-precision natural number.

            This function is overridden at runtime with an efficient implementation.

            Equations
            Instances For
              instance UInt8.instOfNat {n : Nat} :
              Equations

              Converts a UInt16 into the corresponding Fin UInt16.size.

              Equations
              Instances For
                @[deprecated UInt16.toFin (since := "2025-02-12")]

                Converts a UInt16 into the corresponding Fin UInt16.size.

                Equations
                Instances For
                  @[extern lean_uint16_of_nat]

                  Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

                  This function is overridden at runtime with an efficient implementation.

                  Examples:

                  Equations
                  Instances For

                    Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if the number is too large.

                    Returns 2^16 - 1 for natural numbers greater than or equal to 2^16.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Nat.toUInt16 (n : Nat) :

                      Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

                      This function is overridden at runtime with an efficient implementation.

                      Examples:

                      Equations
                      Instances For
                        @[extern lean_uint16_to_nat]

                        Converts a 16-bit unsigned integer to an arbitrary-precision natural number.

                        This function is overridden at runtime with an efficient implementation.

                        Equations
                        Instances For
                          @[extern lean_uint16_to_uint8]

                          Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

                          This function is overridden at runtime with an efficient implementation.

                          Equations
                          Instances For
                            @[extern lean_uint8_to_uint16]

                            Converts 8-bit unsigned integers to 16-bit unsigned integers.

                            This function is overridden at runtime with an efficient implementation.

                            Equations
                            Instances For
                              instance UInt16.instOfNat {n : Nat} :
                              Equations

                              Converts a UInt32 into the corresponding Fin UInt32.size.

                              Equations
                              Instances For
                                @[deprecated UInt32.toFin (since := "2025-02-12")]

                                Converts a UInt32 into the corresponding Fin UInt32.size.

                                Equations
                                Instances For
                                  @[extern lean_uint32_of_nat]

                                  Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

                                  This function is overridden at runtime with an efficient implementation.

                                  Examples:

                                  Equations
                                  Instances For
                                    @[inline, deprecated UInt32.ofNatLT (since := "2025-02-13")]
                                    def UInt32.ofNat' (n : Nat) (h : n < size) :

                                    Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small enough to be representable without overflow; it must be smaller than 2^32.

                                    This function is overridden at runtime with an efficient implementation.

                                    Equations
                                    Instances For

                                      Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if the number is too large.

                                      Returns 2^32 - 1 for natural numbers greater than or equal to 2^32.

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev Nat.toUInt32 (n : Nat) :

                                        Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

                                        This function is overridden at runtime with an efficient implementation.

                                        Examples:

                                        Equations
                                        Instances For
                                          @[extern lean_uint32_to_uint8]

                                          Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.

                                          This function is overridden at runtime with an efficient implementation.

                                          Equations
                                          Instances For
                                            @[extern lean_uint32_to_uint16]

                                            Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

                                            This function is overridden at runtime with an efficient implementation.

                                            Equations
                                            Instances For
                                              @[extern lean_uint8_to_uint32]

                                              Converts 8-bit unsigned integers to 32-bit unsigned integers.

                                              This function is overridden at runtime with an efficient implementation.

                                              Equations
                                              Instances For
                                                @[extern lean_uint16_to_uint32]

                                                Converts 16-bit unsigned integers to 32-bit unsigned integers.

                                                This function is overridden at runtime with an efficient implementation.

                                                Equations
                                                Instances For
                                                  instance UInt32.instOfNat {n : Nat} :
                                                  Equations
                                                  theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) :
                                                  n < mofNatLT n h1 < ofNat m
                                                  @[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]
                                                  theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) :
                                                  n < mofNatLT n h1 < ofNat m
                                                  theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) :
                                                  m < nofNat m < ofNatLT n h1
                                                  @[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]
                                                  theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) :
                                                  m < nofNat m < ofNatLT n h1

                                                  Converts a UInt64 into the corresponding Fin UInt64.size.

                                                  Equations
                                                  Instances For
                                                    @[deprecated UInt64.toFin (since := "2025-02-12")]

                                                    Converts a UInt64 into the corresponding Fin UInt64.size.

                                                    Equations
                                                    Instances For
                                                      @[extern lean_uint64_of_nat]

                                                      Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

                                                      This function is overridden at runtime with an efficient implementation.

                                                      Examples:

                                                      Equations
                                                      Instances For

                                                        Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if the number is too large.

                                                        Returns 2^64 - 1 for natural numbers greater than or equal to 2^64.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev Nat.toUInt64 (n : Nat) :

                                                          Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

                                                          This function is overridden at runtime with an efficient implementation.

                                                          Examples:

                                                          Equations
                                                          Instances For
                                                            @[extern lean_uint64_to_nat]

                                                            Converts a 64-bit unsigned integer to an arbitrary-precision natural number.

                                                            This function is overridden at runtime with an efficient implementation.

                                                            Equations
                                                            Instances For
                                                              @[extern lean_uint64_to_uint8]

                                                              Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

                                                              This function is overridden at runtime with an efficient implementation.

                                                              Equations
                                                              Instances For
                                                                @[extern lean_uint64_to_uint16]

                                                                Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

                                                                This function is overridden at runtime with an efficient implementation.

                                                                Equations
                                                                Instances For
                                                                  @[extern lean_uint64_to_uint32]

                                                                  Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.

                                                                  This function is overridden at runtime with an efficient implementation.

                                                                  Equations
                                                                  Instances For
                                                                    @[extern lean_uint8_to_uint64]

                                                                    Converts 8-bit unsigned integers to 64-bit unsigned integers.

                                                                    This function is overridden at runtime with an efficient implementation.

                                                                    Equations
                                                                    Instances For
                                                                      @[extern lean_uint16_to_uint64]

                                                                      Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

                                                                      This function is overridden at runtime with an efficient implementation.

                                                                      Equations
                                                                      Instances For
                                                                        @[extern lean_uint32_to_uint64]

                                                                        Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

                                                                        This function is overridden at runtime with an efficient implementation.

                                                                        Equations
                                                                        Instances For
                                                                          instance UInt64.instOfNat {n : Nat} :
                                                                          Equations
                                                                          @[deprecated USize.size_eq (since := "2025-02-24")]
                                                                          theorem usize_size_eq :
                                                                          USize.size = 4294967296 USize.size = 18446744073709551616
                                                                          @[deprecated USize.size_pos (since := "2025-02-24")]
                                                                          @[deprecated USize.size_pos (since := "2024-11-24")]

                                                                          Converts a USize into the corresponding Fin USize.size.

                                                                          Equations
                                                                          Instances For
                                                                            @[deprecated USize.toFin (since := "2025-02-12")]
                                                                            def USize.val (x : USize) :

                                                                            Converts a USize into the corresponding Fin USize.size.

                                                                            Equations
                                                                            Instances For
                                                                              @[extern lean_usize_of_nat]
                                                                              def USize.ofNat (n : Nat) :

                                                                              Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.

                                                                              This function is overridden at runtime with an efficient implementation.

                                                                              Equations
                                                                              Instances For

                                                                                Converts a natural number to USize, returning the largest representable value if the number is too large.

                                                                                Returns USize.size - 1, which is 2^64 - 1 or 2^32 - 1 depending on the platform, for natural numbers greater than or equal to USize.size.

                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline]
                                                                                  abbrev Nat.toUSize (n : Nat) :

                                                                                  Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.

                                                                                  This function is overridden at runtime with an efficient implementation.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[extern lean_usize_to_nat]
                                                                                    def USize.toNat (n : USize) :

                                                                                    Converts a word-sized unsigned integer to an arbitrary-precision natural number.

                                                                                    This function is overridden at runtime with an efficient implementation.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[extern lean_usize_add]
                                                                                      def USize.add (a b : USize) :

                                                                                      Adds two word-sized unsigned integers, wrapping around on overflow. Usually accessed via the + operator.

                                                                                      This function is overridden at runtime with an efficient implementation.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[extern lean_usize_sub]
                                                                                        def USize.sub (a b : USize) :

                                                                                        Subtracts one word-sized-bit unsigned integer from another, wrapping around on underflow. Usually accessed via the - operator.

                                                                                        This function is overridden at runtime with an efficient implementation.

                                                                                        Equations
                                                                                        Instances For
                                                                                          def USize.lt (a b : USize) :

                                                                                          Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the < operator.

                                                                                          Equations
                                                                                          Instances For
                                                                                            def USize.le (a b : USize) :

                                                                                            Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the operator.

                                                                                            Equations
                                                                                            Instances For
                                                                                              instance USize.instOfNat {n : Nat} :
                                                                                              Equations
                                                                                              Equations
                                                                                              Equations
                                                                                              instance instLTUSize :
                                                                                              Equations
                                                                                              instance instLEUSize :
                                                                                              Equations
                                                                                              @[extern lean_usize_dec_lt]
                                                                                              def USize.decLt (a b : USize) :
                                                                                              Decidable (a < b)

                                                                                              Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via the DecidableLT USize instance.

                                                                                              This function is overridden at runtime with an efficient implementation.

                                                                                              Examples:

                                                                                              • (if (6 : USize) < 7 then "yes" else "no") = "yes"
                                                                                              • (if (5 : USize) < 5 then "yes" else "no") = "no"
                                                                                              • show ¬((7 : USize) < 7) by decide
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[extern lean_usize_dec_le]
                                                                                                def USize.decLe (a b : USize) :

                                                                                                Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed via the DecidableLE USize instance.

                                                                                                This function is overridden at runtime with an efficient implementation.

                                                                                                Examples:

                                                                                                • (if (15 : USize) ≤ 15 then "yes" else "no") = "yes"
                                                                                                • (if (15 : USize) ≤ 5 then "yes" else "no") = "no"
                                                                                                • (if (5 : USize) ≤ 15 then "yes" else "no") = "yes"
                                                                                                • show (7 : USize) ≤ 7 by decide
                                                                                                Equations
                                                                                                Instances For
                                                                                                  instance instDecidableLtUSize (a b : USize) :
                                                                                                  Decidable (a < b)
                                                                                                  Equations
                                                                                                  instance instDecidableLeUSize (a b : USize) :
                                                                                                  Equations