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")]

                                                                                                                                                          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]
                                                                                                                                                                                                            instance 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
                                                                                                                                                                                                              @[extern lean_usize_dec_le]
                                                                                                                                                                                                              instance 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