Module docstring
{}
UInt8.ofFin
definition
(a : Fin UInt8.size) : UInt8
Full source
/-- Converts a `Fin UInt8.size` into the corresponding `UInt8`. -/
@[inline] def UInt8.ofFin (a : Fin UInt8.size) : UInt8 := ⟨⟨a⟩⟩Informal description
The function converts a natural number less than 256 (represented as an element of `Fin UInt8.size`) into the corresponding unsigned 8-bit integer.
UInt8.mk
definition
(bitVec : BitVec 8) : UInt8
Full source
@[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec]
def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
UInt8.ofBitVec bitVecInformal description
The function constructs an unsigned 8-bit integer from a bitvector of width 8.
UInt8.ofNatCore
definition
(n : Nat) (h : n < UInt8.size) : UInt8
Full source
@[inline, deprecated UInt8.ofNatLT (since := "2025-02-13"), inherit_doc UInt8.ofNatLT]
def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) : UInt8 :=
UInt8.ofNatLT n hInformal description
Given a natural number \( n \) and a proof that \( n < 256 \), the function returns the corresponding unsigned 8-bit integer with value \( n \). This function ensures that the input number is within the representable range of an 8-bit unsigned integer.
UInt8.add
definition
(a b : UInt8) : UInt8
Full source
/--
Adds two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_add"]
protected def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩Informal description
The function takes two unsigned 8-bit integers $a$ and $b$ and returns their sum modulo $2^8$, wrapping around on overflow. This operation is typically accessed via the `+` operator.
UInt8.sub
definition
(a b : UInt8) : UInt8
Full source
/--
Subtracts one 8-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_sub"]
protected def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩Informal description
The function subtracts two unsigned 8-bit integers $a$ and $b$, returning the result modulo $2^8$ (wrapping around on underflow). This is implemented by converting the inputs to bitvectors of width 8, performing the subtraction, and then converting back to an unsigned 8-bit integer.
UInt8.mul
definition
(a b : UInt8) : UInt8
Full source
/--
Multiplies two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_mul"]
protected def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩Informal description
The function takes two unsigned 8-bit integers \( a \) and \( b \) and returns their product modulo \( 2^8 \), wrapping around on overflow. This is the multiplication operation for 8-bit unsigned integers.
UInt8.div
definition
(a b : UInt8) : UInt8
Full source
/--
Unsigned division for 8-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_div"]
protected def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩Informal description
The function takes two unsigned 8-bit integers $a$ and $b$ and returns their unsigned division (floor division), discarding the remainder. Division by zero is defined to return zero.
UInt8.mod
definition
(a b : UInt8) : UInt8
Full source
/--
The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
When the divisor is `0`, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
* `UInt8.mod 5 2 = 1`
* `UInt8.mod 4 2 = 0`
* `UInt8.mod 4 0 = 4`
-/
@[extern "lean_uint8_mod"]
protected def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩Informal description
The modulo operation for unsigned 8-bit integers, which computes the remainder when dividing $a$ by $b$. If $b = 0$, the result is $a$ instead of an error. This operation is implemented using bitwise operations on the underlying bit-vector representation of the integers.
UInt8.modn
definition
(a : UInt8) (n : Nat) : UInt8
Full source
@[deprecated UInt8.mod (since := "2024-09-23")]
protected def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.toFin n⟩Informal description
The function takes an unsigned 8-bit integer $a$ and a natural number $n$, and returns $a \mod n$ as an unsigned 8-bit integer. This is implemented by first converting $a$ to its underlying finite representation and then applying the modulo operation with $n$.
UInt8.land
definition
(a b : UInt8) : UInt8
Full source
/--
Bitwise and for 8-bit unsigned integers. Usually accessed via the `&&&` operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_land"]
protected def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩Informal description
The bitwise AND operation on two unsigned 8-bit integers \( a \) and \( b \), where each bit of the result is set if and only if the corresponding bits of both \( a \) and \( b \) are set. The operation is implemented by converting the integers to bitvectors, performing the bitwise AND, and then converting back to an unsigned 8-bit integer.
UInt8.lor
definition
(a b : UInt8) : UInt8
Full source
/--
Bitwise or for 8-bit unsigned integers. Usually accessed via the `|||` operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_lor"]
protected def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩Informal description
The bitwise OR operation for 8-bit unsigned integers, denoted by `a ||| b`, returns an 8-bit unsigned integer where each bit is set to 1 if at least one of the corresponding bits in the input integers `a` and `b` is 1, and 0 otherwise.
UInt8.xor
definition
(a b : UInt8) : UInt8
Full source
/--
Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_xor"]
protected def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩Informal description
The bitwise exclusive OR (XOR) operation for unsigned 8-bit integers. Given two 8-bit integers $a$ and $b$, the result is an 8-bit integer where each bit is set to 1 if exactly one of the corresponding bits in $a$ and $b$ is 1, and 0 otherwise. This operation is typically accessed via the `^^^` operator and has an efficient runtime implementation.
UInt8.shiftLeft
definition
(a b : UInt8) : UInt8
Full source
/--
Bitwise left shift for 8-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_shift_left"]
protected def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (UInt8.mod b 8).toBitVec⟩Informal description
The bitwise left shift operation for 8-bit unsigned integers, which shifts the bits of $a$ to the left by $(b \mod 8)$ positions. This operation is typically accessed via the `<<<` operator and has an efficient runtime implementation.
UInt8.shiftRight
definition
(a b : UInt8) : UInt8
Full source
/--
Bitwise right shift for 8-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_shift_right"]
protected def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (UInt8.mod b 8).toBitVec⟩Informal description
The function takes two unsigned 8-bit integers $a$ and $b$ and returns the result of bitwise right-shifting $a$ by $(b \mod 8)$ bits. The shift amount is taken modulo 8 to ensure it is within the valid range for an 8-bit integer.
UInt8.lt
definition
(a b : UInt8) : Prop
Informal description
For two unsigned 8-bit integers $a$ and $b$, the strict inequality $a < b$ holds if and only if the underlying bitvector representation of $a$ is strictly less than that of $b$ when interpreted as natural numbers.
UInt8.le
definition
(a b : UInt8) : Prop
Informal description
For any two unsigned 8-bit integers $a$ and $b$, the relation $a \leq b$ holds if and only if the natural number representation of $a$ is less than or equal to the natural number representation of $b$.
instAddUInt8
instance
: Add UInt8
Full source
instance : Add UInt8 := ⟨UInt8.add⟩Informal description
The type of unsigned 8-bit integers `UInt8` is equipped with an addition operation `+` that performs addition modulo 256 (wrapping around on overflow).
instSubUInt8
instance
: Sub UInt8
Full source
instance : Sub UInt8 := ⟨UInt8.sub⟩Informal description
The type of unsigned 8-bit integers $UInt8$ is equipped with a subtraction operation that computes the difference modulo $2^8$ (with wrap-around on underflow).
instMulUInt8
instance
: Mul UInt8
Full source
instance : Mul UInt8 := ⟨UInt8.mul⟩Informal description
The type of unsigned 8-bit integers $UInt8$ is equipped with a multiplication operation that computes the product modulo $2^8$, wrapping around on overflow.
instModUInt8
instance
: Mod UInt8
Full source
instance : Mod UInt8 := ⟨UInt8.mod⟩Informal description
The unsigned 8-bit integers $\text{UInt8}$ are equipped with a modulo operation $\%$ that computes the remainder when dividing one integer by another. If the divisor is zero, the operation returns the dividend.
instHModUInt8Nat
instance
: HMod UInt8 Nat UInt8
Informal description
For any unsigned 8-bit integer $a$ and natural number $n$, the operation $a \bmod n$ yields an unsigned 8-bit integer result. This defines a heterogeneous modulo operation where the dividend is of type `UInt8` and the modulus is of type `Nat`, producing a result of type `UInt8$.
instDivUInt8
instance
: Div UInt8
Full source
instance : Div UInt8 := ⟨UInt8.div⟩Informal description
The type of unsigned 8-bit integers $\mathtt{UInt8}$ is equipped with a division operation $/$, where for any two elements $a, b \in \mathtt{UInt8}$, the division $a / b$ is computed as floor division (discarding the remainder). Division by zero is defined to return zero.
instLTUInt8
instance
: LT UInt8
Full source
instance : LT UInt8 := ⟨UInt8.lt⟩Informal description
The type of unsigned 8-bit integers $\mathtt{UInt8}$ is equipped with a strict less-than relation $<$, where for any two elements $a, b \in \mathtt{UInt8}$, the relation $a < b$ holds if and only if the underlying bitvector representation of $a$ is strictly less than that of $b$ when interpreted as natural numbers.
instLEUInt8
instance
: LE UInt8
Full source
instance : LE UInt8 := ⟨UInt8.le⟩Informal description
The type of unsigned 8-bit integers $\mathtt{UInt8}$ is equipped with a canonical "less than or equal to" relation $\leq$, where for any two elements $a, b \in \mathtt{UInt8}$, the relation $a \leq b$ holds if and only if the natural number representation of $a$ is less than or equal to the natural number representation of $b$.
UInt8.complement
definition
(a : UInt8) : UInt8
Full source
/--
Bitwise complement, also known as bitwise negation, for 8-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_complement"]
protected def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩Informal description
The bitwise complement (negation) of an unsigned 8-bit integer \( a \), where each bit of the result is the opposite of the corresponding bit in \( a \). This operation is denoted by the `~~~` prefix operator.
UInt8.neg
definition
(a : UInt8) : UInt8
Full source
/--
Negation of 8-bit unsigned integers, computed modulo `UInt8.size`.
`UInt8.neg a` is equivalent to `255 - a + 1`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_neg"]
protected def UInt8.neg (a : UInt8) : UInt8 := ⟨-a.toBitVec⟩Informal description
The negation of an 8-bit unsigned integer \( a \) is computed as \( 255 - a + 1 \), which is equivalent to taking the two's complement of \( a \) modulo \( 256 \). This operation is represented by interpreting \( a \) as a bitvector of width 8 and negating it.
instComplementUInt8
instance
: Complement UInt8
Full source
instance : Complement UInt8 := ⟨UInt8.complement⟩Informal description
The type of unsigned 8-bit integers `UInt8` has a logical complement operation, where for any `a : UInt8`, the complement `~~~a` is defined as the bitwise negation of `a`.
instNegUInt8
instance
: Neg UInt8
Full source
instance : Neg UInt8 := ⟨UInt8.neg⟩Informal description
The type of unsigned 8-bit integers has a negation operation defined by two's complement arithmetic modulo 256.
instAndOpUInt8
instance
: AndOp UInt8
Full source
instance : AndOp UInt8 := ⟨UInt8.land⟩Informal description
The unsigned 8-bit integers $\text{UInt8}$ can be equipped with a homogeneous logical AND operation, where for any two elements $a, b \in \text{UInt8}$, the operation $a \&\&\& b$ is defined as the bitwise AND of $a$ and $b$.
instOrOpUInt8
instance
: OrOp UInt8
Full source
instance : OrOp UInt8 := ⟨UInt8.lor⟩Informal description
The unsigned 8-bit integers $\text{UInt8}$ can be equipped with a homogeneous logical OR operation, where for any two elements $a, b \in \text{UInt8}$, the operation $a \mathbin{|||} b$ is defined as the bitwise OR of $a$ and $b$.
instXorUInt8
instance
: Xor UInt8
Full source
instance : Xor UInt8 := ⟨UInt8.xor⟩Informal description
The unsigned 8-bit integers $\text{UInt8}$ can be equipped with a homogeneous exclusive OR (XOR) operation, where for any two elements $a, b \in \text{UInt8}$, the operation $a \oplus b$ is defined as the bitwise XOR of $a$ and $b$.
instShiftLeftUInt8
instance
: ShiftLeft UInt8
Full source
instance : ShiftLeft UInt8 := ⟨UInt8.shiftLeft⟩Informal description
The unsigned 8-bit integers $\text{UInt8}$ can be equipped with a homogeneous left shift operation, where for any two elements $a, b \in \text{UInt8}$, the operation $a \ll b$ is defined as the bitwise left shift of $a$ by $(b \mod 8)$ positions.
instShiftRightUInt8
instance
: ShiftRight UInt8
Full source
instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩Informal description
The unsigned 8-bit integers $\text{UInt8}$ can be equipped with a homogeneous right shift operation, where for any two elements $a, b \in \text{UInt8}$, the operation $a \gg b$ is defined as the bitwise right shift of $a$ by $(b \mod 8)$ bits.
Bool.toUInt8
definition
(b : Bool) : UInt8
Full source
/--
Converts `true` to `1` and `false` to `0`.
-/
@[extern "lean_bool_to_uint8"]
def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0Informal description
The function converts a boolean value `b` to an unsigned 8-bit integer, returning `1` if `b` is `true` and `0` if `b` is `false`.
UInt8.decLt
definition
(a b : UInt8) : Decidable (a < b)
Full source
/--
Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt8` instance.
This function is overridden at runtime with an efficient implementation.
Examples:
* `(if (6 : UInt8) < 7 then "yes" else "no") = "yes"`
* `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
* `show ¬((7 : UInt8) < 7) by decide`
-/
@[extern "lean_uint8_dec_lt"]
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))Informal description
Given two unsigned 8-bit integers $a$ and $b$, the function decides whether $a < b$ holds by comparing their underlying bitvector representations. This is used to construct a `Decidable` instance for the strict order relation on `UInt8`.
UInt8.decLe
definition
(a b : UInt8) : Decidable (a ≤ b)
Full source
/--
Decides whether one 8-bit unsigned integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt8` instance.
This function is overridden at runtime with an efficient implementation.
Examples:
* `(if (15 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
* `(if (15 : UInt8) ≤ 5 then "yes" else "no") = "no"`
* `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
* `show (7 : UInt8) ≤ 7 by decide`
-/
@[extern "lean_uint8_dec_le"]
def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))Informal description
The function decides whether one unsigned 8-bit integer is less than or equal to another, returning a constructive proof of the decidability of the proposition $a \leq b$ for any $a, b \in \mathtt{UInt8}$. This is typically accessed via the `DecidableLE UInt8` instance and is overridden at runtime with an efficient implementation.
instDecidableLtUInt8
instance
(a b : UInt8) : Decidable (a < b)
Full source
instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a bInformal description
For any two unsigned 8-bit integers $a$ and $b$, the proposition $a < b$ is decidable.
instDecidableLeUInt8
instance
(a b : UInt8) : Decidable (a ≤ b)
Full source
instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a bInformal description
For any two unsigned 8-bit integers $a$ and $b$, the proposition $a \leq b$ is decidable.
instMaxUInt8
instance
: Max UInt8
Informal description
The type of unsigned 8-bit integers $\mathtt{UInt8}$ is equipped with a canonical maximum operation $\max$, where for any two elements $a, b \in \mathtt{UInt8}$, $\max(a, b)$ returns the larger of the two according to the natural ordering on $\mathtt{UInt8}$.
instMinUInt8
instance
: Min UInt8
Informal description
The type of unsigned 8-bit integers $\mathtt{UInt8}$ is equipped with a canonical minimum operation, where for any two elements $a, b \in \mathtt{UInt8}$, the minimum $\min(a, b)$ is defined to be $a$ if $a \leq b$ and $b$ otherwise.
UInt16.ofFin
definition
(a : Fin UInt16.size) : UInt16
Full source
/-- Converts a `Fin UInt16.size` into the corresponding `UInt16`. -/
@[inline] def UInt16.ofFin (a : Fin UInt16.size) : UInt16 := ⟨⟨a⟩⟩Informal description
The function converts a finite natural number $a$ (less than $2^{16}$) into the corresponding unsigned 16-bit integer.
UInt16.mk
definition
(bitVec : BitVec 16) : UInt16
Full source
@[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec]
def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
UInt16.ofBitVec bitVecInformal description
The function constructs an unsigned 16-bit integer from a bitvector of width 16.
UInt16.ofNatCore
definition
(n : Nat) (h : n < UInt16.size) : UInt16
Full source
@[inline, deprecated UInt16.ofNatLT (since := "2025-02-13"), inherit_doc UInt16.ofNatLT]
def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) : UInt16 :=
UInt16.ofNatLT n hInformal description
The function converts a natural number \( n \) to an unsigned 16-bit integer, given a proof that \( n < 2^{16} \).
UInt16.add
definition
(a b : UInt16) : UInt16
Full source
/--
Adds two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_add"]
protected def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩Informal description
The function takes two unsigned 16-bit integers $a$ and $b$ and returns their sum modulo $2^{16}$, wrapping around on overflow. This operation is typically accessed via the $+$ operator.
UInt16.sub
definition
(a b : UInt16) : UInt16
Full source
/--
Subtracts one 16-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_sub"]
protected def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩Informal description
The function subtracts two unsigned 16-bit integers \( a \) and \( b \), wrapping around on underflow. The result is another unsigned 16-bit integer. This operation is typically accessed via the `-` operator and is optimized at runtime for efficiency.
UInt16.mul
definition
(a b : UInt16) : UInt16
Full source
/--
Multiplies two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_mul"]
protected def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩Informal description
The function takes two unsigned 16-bit integers \( a \) and \( b \) and returns their product modulo \( 2^{16} \), wrapping around on overflow. This operation is typically accessed via the \( * \) operator and is optimized at runtime for efficiency.
UInt16.div
definition
(a b : UInt16) : UInt16
Full source
/--
Unsigned division for 16-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_div"]
protected def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩Informal description
The function divides two unsigned 16-bit integers \( a \) and \( b \), discarding the remainder (floor division). Division by zero is defined to return zero. This operation is typically accessed via the `/` operator and is optimized at runtime for efficiency.
UInt16.mod
definition
(a b : UInt16) : UInt16
Full source
/--
The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
When the divisor is `0`, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
* `UInt16.mod 5 2 = 1`
* `UInt16.mod 4 2 = 0`
* `UInt16.mod 4 0 = 4`
-/
@[extern "lean_uint16_mod"]
protected def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩Informal description
The modulo operation for 16-bit unsigned integers, which computes the remainder when dividing $a$ by $b$. If $b = 0$, the result is $a$ instead of an error. This operation is denoted by the `%` symbol in practice.
UInt16.modn
definition
(a : UInt16) (n : Nat) : UInt16
Full source
@[deprecated UInt16.mod (since := "2024-09-23")]
protected def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.toFin n⟩Informal description
The function takes a 16-bit unsigned integer `a` and a natural number `n`, and returns the result of `a` modulo `n` as another 16-bit unsigned integer. This is implemented by converting `a` to its underlying finite representation and applying the modulo operation.
UInt16.land
definition
(a b : UInt16) : UInt16
Full source
/--
Bitwise and for 16-bit unsigned integers. Usually accessed via the `&&&` operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_land"]
protected def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩Informal description
The bitwise AND operation on two unsigned 16-bit integers \( a \) and \( b \), where each bit of the result is set to 1 if and only if the corresponding bits of both \( a \) and \( b \) are 1. The operation is implemented by converting the integers to bitvectors and applying the bitwise AND operation on them.
UInt16.lor
definition
(a b : UInt16) : UInt16
Full source
/--
Bitwise or for 16-bit unsigned integers. Usually accessed via the `|||` operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_lor"]
protected def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩Informal description
The bitwise OR operation on two unsigned 16-bit integers \( a \) and \( b \), where each bit of the result is set to 1 if at least one of the corresponding bits of \( a \) or \( b \) is 1. The operation is implemented by converting the integers to bitvectors and applying the bitwise OR operation on them.
UInt16.xor
definition
(a b : UInt16) : UInt16
Full source
/--
Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_xor"]
protected def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩Informal description
The bitwise exclusive OR (XOR) operation on two unsigned 16-bit integers \( a \) and \( b \). Each bit of the resulting integer is set to 1 if exactly one of the corresponding bits of \( a \) and \( b \) is 1, and 0 otherwise. The operation is implemented by converting the integers to bitvectors and applying the bitwise XOR operation on them.
UInt16.shiftLeft
definition
(a b : UInt16) : UInt16
Full source
/--
Bitwise left shift for 16-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_shift_left"]
protected def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (UInt16.mod b 16).toBitVec⟩Informal description
The bitwise left shift operation for unsigned 16-bit integers, which shifts the bits of \( a \) to the left by \( b \mod 16 \) positions. This operation is typically accessed via the `<<<` operator and has an efficient runtime implementation.
UInt16.shiftRight
definition
(a b : UInt16) : UInt16
Full source
/--
Bitwise right shift for 16-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_shift_right"]
protected def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (UInt16.mod b 16).toBitVec⟩Informal description
The bitwise right shift operation for unsigned 16-bit integers, which shifts the bits of $a$ to the right by $b \bmod 16$ positions. This operation is typically accessed via the `>>>` operator and is implemented efficiently at runtime.
UInt16.lt
definition
(a b : UInt16) : Prop
Informal description
For two unsigned 16-bit integers $a$ and $b$, the strict inequality $a < b$ holds if and only if the natural number representation of $a$ is strictly less than the natural number representation of $b$.
UInt16.le
definition
(a b : UInt16) : Prop
Informal description
For any two unsigned 16-bit integers $a$ and $b$, the relation $a \leq b$ holds if and only if the natural number representation of $a$ is less than or equal to the natural number representation of $b$.
instAddUInt16
instance
: Add UInt16
Full source
instance : Add UInt16 := ⟨UInt16.add⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with an addition operation $+$ that computes the sum modulo $2^{16}$, wrapping around on overflow.
instSubUInt16
instance
: Sub UInt16
Full source
instance : Sub UInt16 := ⟨UInt16.sub⟩Informal description
The type of unsigned 16-bit integers `UInt16` is equipped with a subtraction operation that wraps around on underflow.
instMulUInt16
instance
: Mul UInt16
Full source
instance : Mul UInt16 := ⟨UInt16.mul⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a multiplication operation that computes the product modulo $2^{16}$, wrapping around on overflow.
instModUInt16
instance
: Mod UInt16
Full source
instance : Mod UInt16 := ⟨UInt16.mod⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ have a modulo operation `%` defined by $a \% b$ which computes the remainder when $a$ is divided by $b$. If $b = 0$, the result is $a$.
instHModUInt16Nat
instance
: HMod UInt16 Nat UInt16
Informal description
For any 16-bit unsigned integer $a$ and natural number $n$, the operation $a \bmod n$ yields another 16-bit unsigned integer. This defines a heterogeneous modulo operation where the dividend and modulus are of different types (UInt16 and Nat respectively), but the result is of the same type as the dividend (UInt16).
instDivUInt16
instance
: Div UInt16
Full source
instance : Div UInt16 := ⟨UInt16.div⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a division operation $/$ that performs floor division, where division by zero is defined to return zero.
instLTUInt16
instance
: LT UInt16
Full source
instance : LT UInt16 := ⟨UInt16.lt⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a strict order relation $<$, where $a < b$ holds if and only if the natural number representation of $a$ is strictly less than that of $b$.
instLEUInt16
instance
: LE UInt16
Full source
instance : LE UInt16 := ⟨UInt16.le⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a canonical "less than or equal to" relation $\leq$, defined by comparing their underlying natural number representations.
UInt16.complement
definition
(a : UInt16) : UInt16
Full source
/--
Bitwise complement, also known as bitwise negation, for 16-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_complement"]
protected def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩Informal description
The bitwise complement (negation) of a 16-bit unsigned integer \( a \), where each bit of the result is the opposite of the corresponding bit in \( a \). This operation is typically accessed using the `~~~` prefix operator.
UInt16.neg
definition
(a : UInt16) : UInt16
Full source
/--
Negation of 16-bit unsigned integers, computed modulo `UInt16.size`.
`UInt16.neg a` is equivalent to `65_535 - a + 1`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_neg"]
protected def UInt16.neg (a : UInt16) : UInt16 := ⟨-a.toBitVec⟩Informal description
The negation of a 16-bit unsigned integer \( a \) is computed as \( 65535 - a + 1 \), which is equivalent to taking the two's complement of \( a \) modulo \( 2^{16} \).
instComplementUInt16
instance
: Complement UInt16
Full source
instance : Complement UInt16 := ⟨UInt16.complement⟩Informal description
The type of 16-bit unsigned integers has a logical complement operation, where each bit of the integer is flipped.
instNegUInt16
instance
: Neg UInt16
Full source
instance : Neg UInt16 := ⟨UInt16.neg⟩Informal description
The type of unsigned 16-bit integers has a negation operation defined by two's complement arithmetic modulo $2^{16}$.
instAndOpUInt16
instance
: AndOp UInt16
Full source
instance : AndOp UInt16 := ⟨UInt16.land⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a homogeneous logical AND operation `&&&`, where for any two elements $a, b \in \text{UInt16}$, the operation $a \&\&\& b$ is defined as their bitwise AND.
instOrOpUInt16
instance
: OrOp UInt16
Full source
instance : OrOp UInt16 := ⟨UInt16.lor⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a bitwise OR operation $\|$, where for any two elements $a$ and $b$ in $\text{UInt16}$, $a \| b$ computes the bitwise OR of $a$ and $b$.
instXorUInt16
instance
: Xor UInt16
Full source
instance : Xor UInt16 := ⟨UInt16.xor⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a bitwise exclusive OR (XOR) operation, where for any two elements $a$ and $b$ in $\text{UInt16}$, the result $a \oplus b$ is computed by applying the XOR operation bitwise.
instShiftLeftUInt16
instance
: ShiftLeft UInt16
Full source
instance : ShiftLeft UInt16 := ⟨UInt16.shiftLeft⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a left shift operation $\ll$, where for any element $a$ in $\text{UInt16}$ and shift amount $b$, the operation $a \ll b$ shifts the bits of $a$ left by $b \mod 16$ positions.
instShiftRightUInt16
instance
: ShiftRight UInt16
Full source
instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a homogeneous right shift operation $\ggg$, where for any $a, b \in \text{UInt16}$, the operation $a \ggg b$ shifts the bits of $a$ to the right by $b \bmod 16$ positions.
Bool.toUInt16
definition
(b : Bool) : UInt16
Full source
/--
Converts `true` to `1` and `false` to `0`.
-/
@[extern "lean_bool_to_uint16"]
def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0Informal description
The function converts a boolean value `b` to an unsigned 16-bit integer, mapping `true` to `1` and `false` to `0`.
UInt16.decLt
definition
(a b : UInt16) : Decidable (a < b)
Full source
/--
Decides whether one 16-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt16` instance.
This function is overridden at runtime with an efficient implementation.
Examples:
* `(if (6 : UInt16) < 7 then "yes" else "no") = "yes"`
* `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
* `show ¬((7 : UInt16) < 7) by decide`
-/
@[extern "lean_uint16_dec_lt"]
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))Informal description
The function `UInt16.decLt` decides whether one unsigned 16-bit integer is strictly less than another by comparing their underlying bitvector representations. This is typically accessed via the `DecidableLT UInt16` instance and is overridden at runtime with an efficient implementation.
Examples:
- `(6 : UInt16) < 7` evaluates to `true`
- `(5 : UInt16) < 5` evaluates to `false`
- `¬((7 : UInt16) < 7)` holds by definition
UInt16.decLe
definition
(a b : UInt16) : Decidable (a ≤ b)
Full source
/--
Decides whether one 16-bit unsigned integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt16` instance.
This function is overridden at runtime with an efficient implementation.
Examples:
* `(if (15 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
* `(if (15 : UInt16) ≤ 5 then "yes" else "no") = "no"`
* `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
* `show (7 : UInt16) ≤ 7 by decide`
-/
@[extern "lean_uint16_dec_le"]
def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))Informal description
The function that decides whether one unsigned 16-bit integer is less than or equal to another, by converting them to bitvectors and using the decidability instance for bitvector ordering.
instDecidableLtUInt16
instance
(a b : UInt16) : Decidable (a < b)
Full source
instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a bInformal description
For any two unsigned 16-bit integers $a$ and $b$, the proposition $a < b$ is decidable. This means there exists a constructive procedure to determine whether $a$ is strictly less than $b$ by comparing their underlying bitvector representations.
instDecidableLeUInt16
instance
(a b : UInt16) : Decidable (a ≤ b)
Full source
instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a bInformal description
For any two unsigned 16-bit integers $a$ and $b$, the proposition $a \leq b$ is decidable.
instMaxUInt16
instance
: Max UInt16
Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a canonical maximum operation $\max$, defined by comparing their underlying natural number representations.
instMinUInt16
instance
: Min UInt16
Informal description
The unsigned 16-bit integers $\text{UInt16}$ are equipped with a minimum operation, where the minimum of two elements $a$ and $b$ is defined to be $a$ if $a \leq b$ and $b$ otherwise.
UInt32.ofFin
definition
(a : Fin UInt32.size) : UInt32
Full source
/-- Converts a `Fin UInt32.size` into the corresponding `UInt32`. -/
@[inline] def UInt32.ofFin (a : Fin UInt32.size) : UInt32 := ⟨⟨a⟩⟩Informal description
The function converts a finite natural number $a$ (where $a < 2^{32}$) into the corresponding unsigned 32-bit integer.
UInt32.mk
definition
(bitVec : BitVec 32) : UInt32
Full source
@[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec]
def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
UInt32.ofBitVec bitVecInformal description
The function constructs an unsigned 32-bit integer from a bitvector of width 32.
UInt32.ofNatCore
definition
(n : Nat) (h : n < UInt32.size) : UInt32
Full source
@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) : UInt32 :=
UInt32.ofNatLT n hInformal description
Given a natural number \( n \) and a proof that \( n < 2^{32} \), the function returns the corresponding unsigned 32-bit integer representation of \( n \).
UInt32.add
definition
(a b : UInt32) : UInt32
Full source
/--
Adds two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_add"]
protected def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩Informal description
The function takes two unsigned 32-bit integers \( a \) and \( b \) and returns their sum modulo \( 2^{32} \), wrapping around on overflow. This is implemented by converting the integers to bitvectors of width 32, performing bitvector addition, and then converting back to a 32-bit unsigned integer.
UInt32.sub
definition
(a b : UInt32) : UInt32
Full source
/--
Subtracts one 32-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_sub"]
protected def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩Informal description
The function subtracts one unsigned 32-bit integer $b$ from another $a$, returning the result as another unsigned 32-bit integer. If the result underflows (i.e., would be negative), it wraps around modulo $2^{32}$.
UInt32.mul
definition
(a b : UInt32) : UInt32
Full source
/--
Multiplies two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_mul"]
protected def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩Informal description
The function multiplies two unsigned 32-bit integers $a$ and $b$, returning their product modulo $2^{32}$ (i.e., wrapping around on overflow). The operation is implemented using bitvector multiplication.
UInt32.div
definition
(a b : UInt32) : UInt32
Full source
/--
Unsigned division for 32-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_div"]
protected def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩Informal description
The function takes two unsigned 32-bit integers \( a \) and \( b \) and returns the unsigned floor division of \( a \) by \( b \), discarding the remainder. Division by zero is defined to return zero.
UInt32.mod
definition
(a b : UInt32) : UInt32
Full source
/--
The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
When the divisor is `0`, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
* `UInt32.mod 5 2 = 1`
* `UInt32.mod 4 2 = 0`
* `UInt32.mod 4 0 = 4`
-/
@[extern "lean_uint32_mod"]
protected def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩Informal description
The modulo operation for unsigned 32-bit integers, which computes the remainder when dividing $a$ by $b$. If $b = 0$, the result is $a$ instead of an error.
UInt32.modn
definition
(a : UInt32) (n : Nat) : UInt32
Full source
@[deprecated UInt32.mod (since := "2024-09-23")]
protected def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.toFin n⟩Informal description
The function takes an unsigned 32-bit integer $a$ and a natural number $n$, and returns the remainder when $a$ is divided by $n$, represented as an unsigned 32-bit integer. This is computed by first converting $a$ to its underlying finite type representation and then applying the modulo operation with $n$.
UInt32.land
definition
(a b : UInt32) : UInt32
Full source
/--
Bitwise and for 32-bit unsigned integers. Usually accessed via the `&&&` operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_land"]
protected def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩Informal description
The function takes two unsigned 32-bit integers \( a \) and \( b \) and returns their bitwise AND, where each bit of the result is set if and only if the corresponding bits of both \( a \) and \( b \) are set. This operation is typically accessed via the `&&&` operator.
UInt32.lor
definition
(a b : UInt32) : UInt32
Full source
/--
Bitwise or for 32-bit unsigned integers. Usually accessed via the `|||` operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_lor"]
protected def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩Informal description
The bitwise OR operation on two 32-bit unsigned integers \( a \) and \( b \), where each bit of the result is set to 1 if at least one of the corresponding bits in \( a \) or \( b \) is 1, and 0 otherwise. The operation is implemented by converting the integers to bitvectors, performing the OR operation on the bitvectors, and then converting back to a 32-bit unsigned integer.
UInt32.xor
definition
(a b : UInt32) : UInt32
Full source
/--
Bitwise exclusive or for 32-bit unsigned integers. Usually accessed via the `^^^` operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_xor"]
protected def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩Informal description
The bitwise exclusive OR (XOR) operation for 32-bit unsigned integers, where each bit of the result is set if exactly one of the corresponding bits of the input integers \( a \) and \( b \) is set. This operation is typically accessed via the `^^^` operator.
UInt32.shiftLeft
definition
(a b : UInt32) : UInt32
Full source
/--
Bitwise left shift for 32-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_shift_left"]
protected def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (UInt32.mod b 32).toBitVec⟩Informal description
The function takes two unsigned 32-bit integers \( a \) and \( b \), and returns the result of left-shifting the bits of \( a \) by \( b \mod 32 \) positions. This operation is typically accessed via the `<<<` operator.
UInt32.shiftRight
definition
(a b : UInt32) : UInt32
Full source
/--
Bitwise right shift for 32-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_shift_right"]
protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UInt32.mod b 32).toBitVec⟩Informal description
The function takes two unsigned 32-bit integers \( a \) and \( b \), and returns the result of right-shifting the bits of \( a \) by \( b \mod 32 \) positions. This operation is typically accessed via the `>>>` operator.
UInt32.lt
definition
(a b : UInt32) : Prop
Informal description
For two unsigned 32-bit integers $a$ and $b$, the strict inequality $a < b$ holds if and only if the natural number representation of $a$ is less than the natural number representation of $b$.
UInt32.le
definition
(a b : UInt32) : Prop
Informal description
For two unsigned 32-bit integers \( a \) and \( b \), the relation \( a \leq b \) holds if and only if the natural number representation of \( a \) is less than or equal to the natural number representation of \( b \).
instAddUInt32
instance
: Add UInt32
Full source
instance : Add UInt32 := ⟨UInt32.add⟩Informal description
The type of unsigned 32-bit integers has an addition operation defined by wrapping around on overflow.
instSubUInt32
instance
: Sub UInt32
Full source
instance : Sub UInt32 := ⟨UInt32.sub⟩Informal description
The type of unsigned 32-bit integers has a subtraction operation that returns another unsigned 32-bit integer, with wrap-around behavior when the result would be negative.
instMulUInt32
instance
: Mul UInt32
Full source
instance : Mul UInt32 := ⟨UInt32.mul⟩Informal description
The type of unsigned 32-bit integers $UInt32$ is equipped with a multiplication operation that multiplies two elements and wraps around modulo $2^{32}$.
instModUInt32
instance
: Mod UInt32
Full source
instance : Mod UInt32 := ⟨UInt32.mod⟩Informal description
The unsigned 32-bit integers $\text{UInt32}$ have a modulo operation $\%$ defined on them, which computes the remainder when dividing one unsigned 32-bit integer by another. If the divisor is zero, the operation returns the dividend instead of raising an error.
instHModUInt32Nat
instance
: HMod UInt32 Nat UInt32
Informal description
For an unsigned 32-bit integer $a$ and a natural number $n$, the operation $a \bmod n$ computes the remainder when $a$ is divided by $n$, and returns it as an unsigned 32-bit integer.
instDivUInt32
instance
: Div UInt32
Full source
instance : Div UInt32 := ⟨UInt32.div⟩Informal description
The unsigned 32-bit integers $\text{UInt32}$ are equipped with a division operation $/$, where for any two elements $a, b \in \text{UInt32}$, the division $a / b$ is defined as the floor division of $a$ by $b$ (discarding the remainder), with division by zero defined to return zero.
instLTUInt32_1
instance
: LT UInt32
Full source
instance : LT UInt32 := ⟨UInt32.lt⟩Informal description
The unsigned 32-bit integers $\text{UInt32}$ are equipped with a strict order relation $<$, where for any two elements $a, b \in \text{UInt32}$, the relation $a < b$ holds if and only if the natural number representation of $a$ is less than that of $b$.
instLEUInt32_1
instance
: LE UInt32
Full source
instance : LE UInt32 := ⟨UInt32.le⟩Informal description
The type of unsigned 32-bit integers $\text{UInt32}$ is equipped with a canonical "less than or equal to" relation $\leq$, where for any two elements $a, b \in \text{UInt32}$, the relation $a \leq b$ holds if and only if the natural number representation of $a$ is less than or equal to the natural number representation of $b$.
UInt32.complement
definition
(a : UInt32) : UInt32
Full source
/--
Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_complement"]
protected def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩Informal description
The bitwise complement (negation) of a 32-bit unsigned integer \( a \), where each bit of the result is the opposite of the corresponding bit in \( a \). This operation is typically denoted by the prefix operator `~~~`.
UInt32.neg
definition
(a : UInt32) : UInt32
Full source
/--
Negation of 32-bit unsigned integers, computed modulo `UInt32.size`.
`UInt32.neg a` is equivalent to `429_4967_295 - a + 1`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_neg"]
protected def UInt32.neg (a : UInt32) : UInt32 := ⟨-a.toBitVec⟩Informal description
The negation of a 32-bit unsigned integer \( a \) is computed as \( 2^{32} - a \), which is equivalent to taking the two's complement of \( a \). This operation is performed modulo \( 2^{32} \).
instComplementUInt32
instance
: Complement UInt32
Full source
instance : Complement UInt32 := ⟨UInt32.complement⟩Informal description
The type of unsigned 32-bit integers has a logical complement operation, where each bit of the integer is negated.
instNegUInt32
instance
: Neg UInt32
Full source
instance : Neg UInt32 := ⟨UInt32.neg⟩Informal description
The type of unsigned 32-bit integers has a negation operation defined by $a \mapsto 2^{32} - a$ (computed modulo $2^{32}$).
instAndOpUInt32
instance
: AndOp UInt32
Full source
instance : AndOp UInt32 := ⟨UInt32.land⟩Informal description
The type `UInt32` of unsigned 32-bit integers is equipped with a homogeneous logical AND operation `&&&`, which performs a bitwise AND on its operands.
instOrOpUInt32
instance
: OrOp UInt32
Full source
instance : OrOp UInt32 := ⟨UInt32.lor⟩Informal description
The type of unsigned 32-bit integers `UInt32` is equipped with a homogeneous bitwise OR operation `|||`, where for any two elements `a` and `b` in `UInt32`, the operation `a ||| b` performs a bitwise OR on their binary representations.
instXorUInt32
instance
: Xor UInt32
Full source
instance : Xor UInt32 := ⟨UInt32.xor⟩Informal description
The type of unsigned 32-bit integers has a bitwise XOR operation, where for any two elements $a$ and $b$, the operation $a \oplus b$ computes the bitwise exclusive OR of $a$ and $b$.
instShiftLeftUInt32
instance
: ShiftLeft UInt32
Full source
instance : ShiftLeft UInt32 := ⟨UInt32.shiftLeft⟩Informal description
The type of unsigned 32-bit integers `UInt32` is equipped with a left shift operation `<<<`, where for any two elements `a` and `b` in `UInt32`, the operation `a <<< b` performs a left shift of the bits of `a` by `b mod 32` positions.
instShiftRightUInt32
instance
: ShiftRight UInt32
Full source
instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩Informal description
The type of unsigned 32-bit integers has a right shift operation `>>>`, where for any two elements $a$ and $b$, the operation $a \gg b$ computes the right shift of $a$ by $b \mod 32$ bits.
Bool.toUInt32
definition
(b : Bool) : UInt32
Full source
/--
Converts `true` to `1` and `false` to `0`.
-/
@[extern "lean_bool_to_uint32"]
def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0Informal description
The function converts a boolean value `b` to an unsigned 32-bit integer, returning `1` if `b` is `true` and `0` if `b` is `false`.
UInt64.ofFin
definition
(a : Fin UInt64.size) : UInt64
Full source
/-- Converts a `Fin UInt64.size` into the corresponding `UInt64`. -/
@[inline] def UInt64.ofFin (a : Fin UInt64.size) : UInt64 := ⟨⟨a⟩⟩Informal description
The function converts a natural number $a$ less than $2^{64}$ (represented as an element of `Fin UInt64.size`) to the corresponding unsigned 64-bit integer.
UInt64.mk
definition
(bitVec : BitVec 64) : UInt64
Full source
@[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec]
def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
UInt64.ofBitVec bitVecInformal description
The function constructs an unsigned 64-bit integer from a bitvector of width 64.
UInt64.ofNatCore
definition
(n : Nat) (h : n < UInt64.size) : UInt64
Full source
@[inline, deprecated UInt64.ofNatLT (since := "2025-02-13"), inherit_doc UInt64.ofNatLT]
def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) : UInt64 :=
UInt64.ofNatLT n hInformal description
Given a natural number \( n \) and a proof that \( n < 2^{64} \), the function returns the corresponding unsigned 64-bit integer representation of \( n \). This is an internal implementation detail of `UInt64.ofNatLT`.
UInt64.add
definition
(a b : UInt64) : UInt64
Full source
/--
Adds two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_add"]
protected def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩Informal description
The function takes two unsigned 64-bit integers \( a \) and \( b \) and returns their sum modulo \( 2^{64} \), wrapping around on overflow.
UInt64.sub
definition
(a b : UInt64) : UInt64
Full source
/--
Subtracts one 64-bit unsigned integer from another, wrapping around on underflow. Usually accessed
via the `-` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_sub"]
protected def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩Informal description
The function subtracts two unsigned 64-bit integers \( a \) and \( b \), returning the result modulo \( 2^{64} \) (wrapping around on underflow). This operation is typically accessed via the `-` operator.
UInt64.mul
definition
(a b : UInt64) : UInt64
Full source
/--
Multiplies two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the `*`
operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_mul"]
protected def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩Informal description
The function takes two unsigned 64-bit integers $a$ and $b$ and returns their product modulo $2^{64}$, wrapping around on overflow. This operation is typically accessed via the `*` operator and has an efficient runtime implementation.
UInt64.div
definition
(a b : UInt64) : UInt64
Full source
/--
Unsigned division for 64-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_div"]
protected def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩Informal description
The function takes two unsigned 64-bit integers $a$ and $b$ and returns the unsigned 64-bit integer result of dividing $a$ by $b$, discarding the remainder (floor division). Division by zero is defined to return zero.
UInt64.mod
definition
(a b : UInt64) : UInt64
Full source
/--
The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
When the divisor is `0`, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
* `UInt64.mod 5 2 = 1`
* `UInt64.mod 4 2 = 0`
* `UInt64.mod 4 0 = 4`
-/
@[extern "lean_uint64_mod"]
protected def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩Informal description
The modulo operation for 64-bit unsigned integers, which computes the remainder when dividing $a$ by $b$. If $b = 0$, the result is $a$ instead of an error. This operation is implemented efficiently at runtime.
UInt64.modn
definition
(a : UInt64) (n : Nat) : UInt64
Full source
@[deprecated UInt64.mod (since := "2024-09-23")]
protected def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.toFin n⟩Informal description
The function computes the remainder when an unsigned 64-bit integer \( a \) is divided by a natural number \( n \), returning the result as another unsigned 64-bit integer. This is implemented by first converting \( a \) to its underlying finite representation and then applying the modulo operation with \( n \).
UInt64.land
definition
(a b : UInt64) : UInt64
Full source
/--
Bitwise and for 64-bit unsigned integers. Usually accessed via the `&&&` operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_land"]
protected def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩Informal description
The bitwise AND operation on two unsigned 64-bit integers \( a \) and \( b \), where each bit of the result is set to 1 if and only if the corresponding bits of both \( a \) and \( b \) are 1. The operation is performed by converting the integers to bitvectors and applying the bitwise AND operation on them.
UInt64.lor
definition
(a b : UInt64) : UInt64
Full source
/--
Bitwise or for 64-bit unsigned integers. Usually accessed via the `|||` operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_lor"]
protected def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩Informal description
The bitwise OR operation for 64-bit unsigned integers, where each bit of the result is set to 1 if at least one of the corresponding bits in the input integers $a$ and $b$ is 1. This operation is typically accessed via the `|||` operator.
UInt64.xor
definition
(a b : UInt64) : UInt64
Full source
/--
Bitwise exclusive or for 64-bit unsigned integers. Usually accessed via the `^^^` operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_xor"]
protected def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩Informal description
The function takes two 64-bit unsigned integers \( a \) and \( b \) and returns their bitwise exclusive OR (XOR). Each bit in the result is set to 1 if exactly one of the corresponding bits in \( a \) and \( b \) is 1, and 0 otherwise.
UInt64.shiftLeft
definition
(a b : UInt64) : UInt64
Full source
/--
Bitwise left shift for 64-bit unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_shift_left"]
protected def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (UInt64.mod b 64).toBitVec⟩Informal description
The function takes two 64-bit unsigned integers \( a \) and \( b \) and returns the result of shifting \( a \) left by \( b \mod 64 \) bits. This operation is typically accessed via the `<<<` operator and is implemented efficiently at runtime.
UInt64.shiftRight
definition
(a b : UInt64) : UInt64
Full source
/--
Bitwise right shift for 64-bit unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_shift_right"]
protected def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (UInt64.mod b 64).toBitVec⟩Informal description
The function takes two 64-bit unsigned integers \( a \) and \( b \) and returns the result of shifting \( a \) right by \( b \mod 64 \) bits. This operation is typically accessed via the `>>>` operator and is implemented efficiently at runtime.
UInt64.lt
definition
(a b : UInt64) : Prop
Informal description
For two 64-bit unsigned integers $a$ and $b$, the strict inequality $a < b$ holds if and only if the natural number representation of $a$ is strictly less than the natural number representation of $b$.
UInt64.le
definition
(a b : UInt64) : Prop
Informal description
For two 64-bit unsigned integers \( a \) and \( b \), the relation \( a \leq b \) holds if and only if the natural number representation of \( a \) is less than or equal to the natural number representation of \( b \).
instAddUInt64
instance
: Add UInt64
Full source
instance : Add UInt64 := ⟨UInt64.add⟩Informal description
The type of unsigned 64-bit integers $UInt64$ is equipped with an addition operation $+$ that performs addition modulo $2^{64}$ (with wrap-around on overflow).
instSubUInt64
instance
: Sub UInt64
Full source
instance : Sub UInt64 := ⟨UInt64.sub⟩Informal description
The type of unsigned 64-bit integers has a subtraction operation defined by wrapping around modulo $2^{64}$.
instMulUInt64
instance
: Mul UInt64
Full source
instance : Mul UInt64 := ⟨UInt64.mul⟩Informal description
The unsigned 64-bit integers $\mathtt{UInt64}$ are equipped with a multiplication operation that computes the product modulo $2^{64}$, wrapping around on overflow.
instModUInt64
instance
: Mod UInt64
Full source
instance : Mod UInt64 := ⟨UInt64.mod⟩Informal description
The unsigned 64-bit integers $\mathbb{U}_{64}$ have a modulo operation $\%$ that takes two elements $a, b \in \mathbb{U}_{64}$ and returns the remainder of $a$ divided by $b$. If $b = 0$, the result is $a$.
instHModUInt64Nat
instance
: HMod UInt64 Nat UInt64
Informal description
For any unsigned 64-bit integer $a$ and natural number $n$, the operation $a \bmod n$ computes the remainder of $a$ divided by $n$ and returns another unsigned 64-bit integer.
instDivUInt64
instance
: Div UInt64
Full source
instance : Div UInt64 := ⟨UInt64.div⟩Informal description
The unsigned 64-bit integers $\mathbb{U}_{64}$ have a division operation $/$ that takes two elements $a, b \in \mathbb{U}_{64}$ and returns their floor division result in $\mathbb{U}_{64}$. Division by zero is defined to return zero.
instLTUInt64
instance
: LT UInt64
Full source
instance : LT UInt64 := ⟨UInt64.lt⟩Informal description
The unsigned 64-bit integers $\mathbb{U}_{64}$ have a strict order relation $<$, where $a < b$ holds if and only if the natural number interpretation of $a$ is strictly less than that of $b$.
instLEUInt64
instance
: LE UInt64
Full source
instance : LE UInt64 := ⟨UInt64.le⟩Informal description
The type of unsigned 64-bit integers $\mathbb{U}_{64}$ is equipped with a canonical "less than or equal to" relation $\leq$, where for any $a, b \in \mathbb{U}_{64}$, $a \leq b$ holds if and only if the natural number interpretation of $a$ is less than or equal to that of $b$.
UInt64.complement
definition
(a : UInt64) : UInt64
Full source
/--
Bitwise complement, also known as bitwise negation, for 64-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_complement"]
protected def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩Informal description
The bitwise complement (negation) of a 64-bit unsigned integer \( a \), where each bit of the result is the opposite of the corresponding bit in \( a \). This operation is typically accessed via the `~~~` prefix operator and has an efficient runtime implementation.
UInt64.neg
definition
(a : UInt64) : UInt64
Full source
/--
Negation of 32-bit unsigned integers, computed modulo `UInt64.size`.
`UInt64.neg a` is equivalent to `18_446_744_073_709_551_615 - a + 1`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_neg"]
protected def UInt64.neg (a : UInt64) : UInt64 := ⟨-a.toBitVec⟩Informal description
The negation of a 64-bit unsigned integer \( a \) is computed as the two's complement negation modulo \( 2^{64} \), which is equivalent to \( 18,446,744,073,709,551,615 - a + 1 \).
instComplementUInt64
instance
: Complement UInt64
Full source
instance : Complement UInt64 := ⟨UInt64.complement⟩Informal description
The type of unsigned 64-bit integers has a logical complement operation defined by bitwise negation.
instNegUInt64
instance
: Neg UInt64
Full source
instance : Neg UInt64 := ⟨UInt64.neg⟩Informal description
The type of unsigned 64-bit integers $UInt64$ is equipped with a negation operation, where the negation of an element $a$ is computed as its two's complement negation modulo $2^{64}$.
instAndOpUInt64
instance
: AndOp UInt64
Full source
instance : AndOp UInt64 := ⟨UInt64.land⟩Informal description
The unsigned 64-bit integers $\text{UInt64}$ are equipped with a homogeneous logical AND operation, where for any two elements $a, b \in \text{UInt64}$, the operation $a \&\&\& b$ is defined as their bitwise AND.
instOrOpUInt64
instance
: OrOp UInt64
Full source
instance : OrOp UInt64 := ⟨UInt64.lor⟩Informal description
The type of unsigned 64-bit integers $UInt64$ is equipped with a homogeneous bitwise OR operation $|||$, where for any two elements $a$ and $b$ in $UInt64$, the operation $a ||| b$ computes the bitwise OR of $a$ and $b$.
instXorUInt64
instance
: Xor UInt64
Full source
instance : Xor UInt64 := ⟨UInt64.xor⟩Informal description
The type of unsigned 64-bit integers has a bitwise XOR operation defined on it.
instShiftLeftUInt64
instance
: ShiftLeft UInt64
Full source
instance : ShiftLeft UInt64 := ⟨UInt64.shiftLeft⟩Informal description
The type of unsigned 64-bit integers $UInt64$ is equipped with a left shift operation $<<<$, where for any two elements $a$ and $b$ in $UInt64$, the operation $a <<< b$ computes the left shift of $a$ by $b \mod 64$ bits.
instShiftRightUInt64
instance
: ShiftRight UInt64
Full source
instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩Informal description
The type of unsigned 64-bit integers has a homogeneous right shift operation `>>>` defined on it, where both operands and the result are of type `UInt64`.
Bool.toUInt64
definition
(b : Bool) : UInt64
Full source
/--
Converts `true` to `1` and `false` to `0`.
-/
@[extern "lean_bool_to_uint64"]
def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0Informal description
The function maps a boolean value `b` to the unsigned 64-bit integer `1` if `b` is `true` and to `0` if `b` is `false`.
UInt64.decLt
definition
(a b : UInt64) : Decidable (a < b)
Full source
/--
Decides whether one 64-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt64` instance.
This function is overridden at runtime with an efficient implementation.
Examples:
* `(if (6 : UInt64) < 7 then "yes" else "no") = "yes"`
* `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
* `show ¬((7 : UInt64) < 7) by decide`
-/
@[extern "lean_uint64_dec_lt"]
def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))Informal description
The function that decides whether one 64-bit unsigned integer is strictly less than another, returning a constructive proof of the decidability of the proposition \(a < b\). This is typically accessed via the `DecidableLT UInt64` instance and is overridden at runtime with an efficient implementation.
UInt64.decLe
definition
(a b : UInt64) : Decidable (a ≤ b)
Full source
/--
Decides whether one 64-bit unsigned integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt64` instance.
This function is overridden at runtime with an efficient implementation.
Examples:
* `(if (15 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
* `(if (15 : UInt64) ≤ 5 then "yes" else "no") = "no"`
* `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
* `show (7 : UInt64) ≤ 7 by decide`
-/
@[extern "lean_uint64_dec_le"]
def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))Informal description
The function decides whether one 64-bit unsigned integer $a$ is less than or equal to another 64-bit unsigned integer $b$, returning a constructive proof of decidability for the proposition $a \leq b$. This is typically accessed via the `DecidableLE UInt64` instance and is overridden at runtime with an efficient implementation.
instDecidableLtUInt64
instance
(a b : UInt64) : Decidable (a < b)
Full source
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a bInformal description
For any two unsigned 64-bit integers $a$ and $b$, the proposition $a < b$ is decidable.
instDecidableLeUInt64
instance
(a b : UInt64) : Decidable (a ≤ b)
Full source
instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a bInformal description
For any two 64-bit unsigned integers $a$ and $b$, the proposition $a \leq b$ is decidable.
instMaxUInt64
instance
: Max UInt64
Informal description
The type of unsigned 64-bit integers $\mathbb{U}_{64}$ is equipped with a canonical maximum operation $\max$, where for any $a, b \in \mathbb{U}_{64}$, $\max(a, b)$ returns the larger of the two integers according to the natural order on $\mathbb{U}_{64}$.
instMinUInt64
instance
: Min UInt64
Informal description
The type of unsigned 64-bit integers $\mathbb{U}_{64}$ is equipped with a minimum operation, where for any two elements $a$ and $b$, the minimum is defined to be $a$ if $a \leq b$ and $b$ otherwise.
USize.ofFin
definition
(a : Fin USize.size) : USize
Full source
/-- Converts a `Fin USize.size` into the corresponding `USize`. -/
@[inline] def USize.ofFin (a : Fin USize.size) : USize := ⟨⟨a⟩⟩Informal description
The function converts an element of `Fin USize.size` (a natural number less than the platform's maximum unsigned word-size value) to the corresponding `USize` value. Specifically, given a finite natural number `a` bounded by `USize.size`, it returns the platform-dependent unsigned word-size integer representing the same value.
USize.mk
definition
(bitVec : BitVec System.Platform.numBits) : USize
Full source
@[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec]
def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
USize.ofBitVec bitVecInformal description
Given a bitvector `bitVec` of width equal to the platform's word size (either 32 or 64 bits), the function constructs a platform-dependent unsigned word-size integer from it.
USize.ofNatCore
definition
(n : Nat) (h : n < USize.size) : USize
Full source
@[inline, deprecated USize.ofNatLT (since := "2025-02-13"), inherit_doc USize.ofNatLT]
def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
USize.ofNatLT n hInformal description
Given a natural number \( n \) and a proof that \( n \) is less than the maximum value of `USize` (which is platform-dependent, either \(2^{32}\) or \(2^{64}\)), the function returns the corresponding `USize` value representing \( n \).
USize.le_size
theorem
: 2 ^ 32 ≤ USize.size
Full source
@[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_allInformal description
The size of the unsigned word-size integer type `USize` is at least $2^{32} = 4294967296$.
USize.size_le
theorem
: USize.size ≤ 2 ^ 64
Full source
@[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_allInformal description
The size of the unsigned word-size integer type `USize` is less than or equal to $2^{64}$.
usize_size_le
theorem
: USize.size ≤ 18446744073709551616
Full source
@[deprecated USize.size_le (since := "2025-02-24")]
theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
USize.size_leInformal description
The size of the unsigned word-size integer type `USize` is less than or equal to $2^{64} = 18446744073709551616$.
le_usize_size
theorem
: 4294967296 ≤ USize.size
Full source
@[deprecated USize.le_size (since := "2025-02-24")]
theorem le_usize_size : 4294967296 ≤ USize.size :=
USize.le_sizeInformal description
The size of the unsigned word-size integer type `USize` is at least $4294967296$, i.e., $4294967296 \leq \text{USize.size}$.
USize.mul
definition
(a b : USize) : USize
Full source
/--
Multiplies two word-sized unsigned integers, wrapping around on overflow. Usually accessed via the
`*` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_mul"]
protected def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩Informal description
The function multiplies two unsigned word-sized integers \( a \) and \( b \), wrapping around on overflow. The result is represented as another unsigned word-sized integer. The operation is performed by converting the inputs to bitvectors of width equal to the platform's word size, multiplying them, and then converting back to a word-sized integer.
USize.div
definition
(a b : USize) : USize
Full source
/--
Unsigned division for word-sized unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.
This operation is sometimes called “floor division.” Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_div"]
protected def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩Informal description
The unsigned division operation for platform-dependent unsigned word-size integers, which discards the remainder. Division by zero is defined to return zero. This operation is sometimes called "floor division" and is typically accessed via the `/` operator. The function is implemented by converting the operands to bitvectors, performing division on their underlying natural number representations, and then converting back to a `USize`.
USize.mod
definition
(a b : USize) : USize
Full source
/--
The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.
When the divisor is `0`, the result is the dividend rather than an error.
This function is overridden at runtime with an efficient implementation.
Examples:
* `USize.mod 5 2 = 1`
* `USize.mod 4 2 = 0`
* `USize.mod 4 0 = 4`
-/
@[extern "lean_usize_mod"]
protected def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩Informal description
The modulo operation for platform-dependent unsigned word-size integers, which computes the remainder when dividing one integer by another. If the divisor is zero, the result is the dividend instead of an error.
Given two unsigned word-size integers $a$ and $b$, the operation returns $a \mod b$ when $b \neq 0$, and returns $a$ when $b = 0$.
USize.modn
definition
(a : USize) (n : Nat) : USize
Full source
@[deprecated USize.mod (since := "2024-09-23")]
protected def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.toFin n⟩Informal description
The function computes the remainder when dividing a platform-dependent unsigned word-size integer $a$ by a natural number $n$, returning the result as another unsigned word-size integer. The operation is implemented by converting $a$ to a finite integer representation, performing the modulo operation, and converting back to a `USize`.
USize.land
definition
(a b : USize) : USize
Full source
/--
Bitwise and for word-sized unsigned integers. Usually accessed via the `&&&` operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_land"]
protected def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩Informal description
The bitwise AND operation on two platform-dependent unsigned word-size integers `a` and `b`. Each bit of the resulting integer is set to 1 if and only if the corresponding bits of both `a` and `b` are 1. The operation is implemented by converting the integers to bitvectors, performing the bitwise AND, and then converting back to a `USize`.
USize.lor
definition
(a b : USize) : USize
Full source
/--
Bitwise or for word-sized unsigned integers. Usually accessed via the `|||` operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_lor"]
protected def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩Informal description
The bitwise logical OR operation on two word-sized unsigned integers. For each bit position, the result has a 1 if at least one of the corresponding bits in the input integers is 1, and 0 otherwise. The operation is performed by converting the integers to bitvectors and applying the bitwise OR operation on them.
USize.xor
definition
(a b : USize) : USize
Full source
/--
Bitwise exclusive or for word-sized unsigned integers. Usually accessed via the `^^^` operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_xor"]
protected def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩Informal description
The bitwise exclusive OR (XOR) operation for platform-dependent unsigned word-size integers. Given two integers \( a \) and \( b \), each bit of the result is set to 1 if exactly one of the corresponding bits in \( a \) and \( b \) is 1, and 0 otherwise. This operation is implemented by converting the integers to bitvectors, performing the XOR operation on them, and then converting back to a `USize`.
USize.shiftLeft
definition
(a b : USize) : USize
Full source
/--
Bitwise left shift for word-sized unsigned integers. Usually accessed via the `<<<` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_shift_left"]
protected def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (USize.mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩Informal description
The bitwise left shift operation for platform-dependent unsigned word-size integers. Given two integers $a$ and $b$, the operation shifts the bits of $a$ to the left by $b \mod w$ positions, where $w$ is the platform word size (32 or 64 bits). The bits shifted out are discarded, and zeros are shifted in from the right.
USize.shiftRight
definition
(a b : USize) : USize
Full source
/--
Bitwise right shift for word-sized unsigned integers. Usually accessed via the `>>>` operator.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_shift_right"]
protected def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (USize.mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩Informal description
The bitwise right shift operation for platform-dependent unsigned word-size integers. Given two integers $a$ and $b$, the operation shifts the bits of $a$ to the right by $b \mod w$ positions, where $w$ is the platform word size (32 or 64 bits). The bits shifted out are discarded, and zeros are shifted in from the left.
USize.ofNat32
definition
(n : @& Nat) (h : n < 4294967296) : USize
Full source
/--
Converts a natural number to a `USize`. Overflow is impossible on any supported platform because
`USize.size` is either `2^32` or `2^64`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
USize.ofNatLT n (Nat.lt_of_lt_of_le h USize.le_size)Informal description
Given a natural number \( n \) and a proof that \( n \) is less than \( 2^{32} \), the function returns the corresponding `USize` value representing \( n \). This conversion is guaranteed to be safe as \( 2^{32} \) is within the bounds of `USize` on all supported platforms.
UInt8.toUSize
definition
(a : UInt8) : USize
Full source
/--
Converts 8-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_to_usize"]
def UInt8.toUSize (a : UInt8) : USize :=
USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))Informal description
The function converts an 8-bit unsigned integer \( a \) to a word-sized unsigned integer by interpreting the bits of \( a \) as a natural number and ensuring it fits within the bounds of a 32-bit unsigned integer (which is always true for 8-bit values). This conversion is optimized at runtime for efficiency.
USize.toUInt8
definition
(a : USize) : UInt8
Full source
/--
Converts word-sized unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_to_uint8"]
def USize.toUInt8 (a : USize) : UInt8 := a.toNat.toUInt8Informal description
The function converts a platform-dependent unsigned word-size integer `a` to an 8-bit unsigned integer by first converting it to a natural number and then truncating it to fit within 8 bits (wrapping around on overflow).
UInt16.toUSize
definition
(a : UInt16) : USize
Full source
/--
Converts 16-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_to_usize"]
def UInt16.toUSize (a : UInt16) : USize :=
USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))Informal description
The function converts a 16-bit unsigned integer $a$ to a platform-dependent unsigned word-size integer by interpreting the bit pattern of $a$ as a natural number and ensuring it fits within the bounds of a 32-bit unsigned integer (which is always true for 16-bit values).
USize.toUInt16
definition
(a : USize) : UInt16
Full source
/--
Converts word-sized unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_to_uint16"]
def USize.toUInt16 (a : USize) : UInt16 := a.toNat.toUInt16Informal description
The function converts a platform-dependent unsigned word-size integer $a$ to a 16-bit unsigned integer by first converting $a$ to a natural number and then to a 16-bit unsigned integer. The conversion wraps around on overflow.
UInt32.toUSize
definition
(a : UInt32) : USize
Full source
/--
Converts 32-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_to_usize"]
def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLtInformal description
The function converts a 32-bit unsigned integer \( a \) to a platform-dependent unsigned word-size integer by first converting \( a \) to its natural number representation and then to a `USize` value, ensuring the result is within 32-bit bounds.
USize.toUInt32
definition
(a : USize) : UInt32
Full source
/--
Converts word-sized unsigned integers to 32-bit unsigned integers. Wraps around on overflow, which
might occur on 64-bit architectures.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_to_uint32"]
def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32Informal description
The function converts a platform-dependent unsigned word-size integer $a$ to a 32-bit unsigned integer by first converting to a natural number and then to a 32-bit unsigned integer. On 64-bit architectures, this conversion may wrap around due to overflow.
UInt64.toUSize
definition
(a : UInt64) : USize
Full source
/--
Converts 64-bit unsigned integers to word-sized unsigned integers. On 32-bit machines, this may
overflow, which results in the value wrapping around (that is, it is reduced modulo `USize.size`).
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_to_usize"]
def UInt64.toUSize (a : UInt64) : USize := a.toNat.toUSizeInformal description
The function converts a 64-bit unsigned integer $a$ to a platform-dependent unsigned word-size integer. On 32-bit systems, this conversion may result in overflow, causing the value to wrap around modulo the maximum value of `USize`.
USize.toUInt64
definition
(a : USize) : UInt64
Full source
/--
Converts word-sized unsigned integers to 32-bit unsigned integers. This cannot overflow because
`USize.size` is either `2^32` or `2^64`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_to_uint64"]
def USize.toUInt64 (a : USize) : UInt64 :=
UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt USize.size_le)Informal description
The function converts a platform-dependent unsigned word-size integer \( a \) to a 64-bit unsigned integer. This conversion is performed by first converting \( a \) to its natural number representation via bitvector extraction, then converting this natural number to a 64-bit unsigned integer. The conversion is guaranteed to succeed without overflow since the maximum value of `USize` (either \( 2^{32} \) or \( 2^{64} \)) is always less than or equal to \( 2^{64} \).
instMulUSize
instance
: Mul USize
Full source
instance : Mul USize := ⟨USize.mul⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a multiplication operation that wraps around on overflow.
instModUSize
instance
: Mod USize
Full source
instance : Mod USize := ⟨USize.mod⟩Informal description
The platform-dependent unsigned word-size integers `USize` have a modulo operation `%` defined on them, which computes the remainder when dividing one integer by another. If the divisor is zero, the result is the dividend.
instHModUSizeNat
instance
: HMod USize Nat USize
Informal description
For any platform-dependent unsigned word-size integer $a$ and natural number $n$, the operation $a \bmod n$ is defined and returns another unsigned word-size integer.
instDivUSize
instance
: Div USize
Full source
instance : Div USize := ⟨USize.div⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a division operation `/` that performs unsigned floor division, where division by zero is defined to return zero.
USize.complement
definition
(a : USize) : USize
Full source
/--
Bitwise complement, also known as bitwise negation, for word-sized unsigned integers. Usually
accessed via the `~~~` prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_complement"]
protected def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩Informal description
The bitwise complement (negation) of a platform-dependent unsigned word-size integer `a`. Each bit of the resulting integer is the opposite of the corresponding bit in `a`. This operation is typically accessed via the `~~~` prefix operator and has an efficient runtime implementation.
USize.neg
definition
(a : USize) : USize
Full source
/--
Negation of word-sized unsigned integers, computed modulo `USize.size`.
This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_neg"]
protected def USize.neg (a : USize) : USize := ⟨-a.toBitVec⟩Informal description
The negation of a word-sized unsigned integer \( a \) is computed as the negation modulo \( 2^w \), where \( w \) is the platform's word size (32 or 64 bits). This operation is represented by converting \( a \) to a bitvector of width \( w \), negating it, and then converting back to a `USize`.
instComplementUSize
instance
: Complement USize
Full source
instance : Complement USize := ⟨USize.complement⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers has a logical complement operation, where each bit of the integer is negated.
instNegUSize
instance
: Neg USize
Full source
instance : Neg USize := ⟨USize.neg⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers has a negation operation defined by taking the two's complement modulo $2^w$, where $w$ is the platform's word size (32 or 64 bits).
instAndOpUSize
instance
: AndOp USize
Full source
instance : AndOp USize := ⟨USize.land⟩Informal description
The platform-dependent unsigned word-size integers `USize` can be equipped with a homogeneous logical AND operation `&&&`, where for any two `USize` values `a` and `b`, the operation `a &&& b` is defined as their bitwise AND.
instOrOpUSize
instance
: OrOp USize
Full source
instance : OrOp USize := ⟨USize.lor⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a homogeneous bitwise OR operation `|||`.
instXorUSize
instance
: Xor USize
Full source
instance : Xor USize := ⟨USize.xor⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a homogeneous bitwise XOR operation `^^^`.
instShiftLeftUSize
instance
: ShiftLeft USize
Full source
instance : ShiftLeft USize := ⟨USize.shiftLeft⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a homogeneous bitwise left shift operation `<<<`.
instShiftRightUSize
instance
: ShiftRight USize
Full source
instance : ShiftRight USize := ⟨USize.shiftRight⟩Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a homogeneous bitwise right shift operation `>>>`.
Bool.toUSize
definition
(b : Bool) : USize
Full source
/--
Converts `true` to `1` and `false` to `0`.
-/
@[extern "lean_bool_to_usize"]
def Bool.toUSize (b : Bool) : USize := if b then 1 else 0Informal description
The function converts a boolean value `b` to an unsigned word-size integer, where `true` is mapped to `1` and `false` is mapped to `0`.
instMaxUSize
instance
: Max USize
Informal description
The type `USize` of platform-dependent unsigned word-size integers is equipped with a maximum operation, where for any two elements `x, y : USize`, the operation returns the larger of the two according to the natural ordering on unsigned integers.
instMinUSize
instance
: Min USize
Informal description
The type `USize` of platform-dependent unsigned word-size integers has a minimum operation, where for any two values `x` and `y`, the minimum is defined as `x` if `x ≤ y` and `y` otherwise.