@[inline]

def UInt8.ofFin (a : Fin size) : UInt8

Converts a Fin UInt8.size into the corresponding UInt8.

Equations

• UInt8.ofFin a = { toBitVec := { toFin := a } }

@[deprecated UInt8.ofBitVec (since := "2025-02-12")]

def UInt8.mk (bitVec : BitVec 8) : UInt8

Creates a UInt8 from a BitVec 8. This function is overridden with a native implementation.

Equations

• UInt8.mk bitVec = { toBitVec := bitVec }

@[inline, deprecated UInt8.ofNatLT (since := "2025-02-13")]

def UInt8.ofNatCore (n : Nat) (h : n < size) : UInt8

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

This function is overridden at runtime with an efficient implementation.

Equations

• UInt8.ofNatCore n h = UInt8.ofNatLT n h

@[extern lean_uint8_add]

def UInt8.add (a b : UInt8) : UInt8

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.

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint8_sub]

def UInt8.sub (a b : UInt8) : UInt8

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.

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint8_mul]

def UInt8.mul (a b : UInt8) : UInt8

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.

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint8_div]

def UInt8.div (a b : UInt8) : UInt8

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.

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint8_mod]

def UInt8.mod (a b : UInt8) : UInt8

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

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt8.mod (since := "2024-09-23")]

def UInt8.modn (a : UInt8) (n : Nat) : UInt8

Equations

• a.modn n = { toBitVec := ↑↑(a.toFin.modn n) }

@[extern lean_uint8_land]

def UInt8.land (a b : UInt8) : UInt8

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.

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint8_lor]

def UInt8.lor (a b : UInt8) : UInt8

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.

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint8_xor]

def UInt8.xor (a b : UInt8) : UInt8

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.

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint8_shift_left]

def UInt8.shiftLeft (a b : UInt8) : UInt8

Bitwise left shift for 8-bit unsigned integers. Usually accessed via the <<< operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 8).toBitVec }

@[extern lean_uint8_shift_right]

def UInt8.shiftRight (a b : UInt8) : UInt8

Bitwise right shift for 8-bit unsigned integers. Usually accessed via the >>> operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 8).toBitVec }

def UInt8.lt (a b : UInt8) : Prop

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

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt8.le (a b : UInt8) : Prop

Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt8 : Add UInt8

Equations

• instAddUInt8 = { add := UInt8.add }

instance instSubUInt8 : Sub UInt8

Equations

• instSubUInt8 = { sub := UInt8.sub }

instance instMulUInt8 : Mul UInt8

Equations

• instMulUInt8 = { mul := UInt8.mul }

instance instModUInt8 : Mod UInt8

Equations

• instModUInt8 = { mod := UInt8.mod }

instance instHModUInt8Nat : HMod UInt8 Nat UInt8

Equations

• instHModUInt8Nat = { hMod := UInt8.modn }

instance instDivUInt8 : Div UInt8

Equations

• instDivUInt8 = { div := UInt8.div }

instance instLTUInt8 : LT UInt8

Equations

• instLTUInt8 = { lt := UInt8.lt }

instance instLEUInt8 : LE UInt8

Equations

• instLEUInt8 = { le := UInt8.le }

@[extern lean_uint8_complement]

def UInt8.complement (a : UInt8) : UInt8

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.

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

@[extern lean_uint8_neg]

def UInt8.neg (a : UInt8) : UInt8

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.

Equations

• a.neg = { toBitVec := -a.toBitVec }

instance instComplementUInt8 : Complement UInt8

Equations

• instComplementUInt8 = { complement := UInt8.complement }

instance instNegUInt8 : Neg UInt8

Equations

• instNegUInt8 = { neg := UInt8.neg }

instance instAndOpUInt8 : AndOp UInt8

Equations

• instAndOpUInt8 = { and := UInt8.land }

instance instOrOpUInt8 : OrOp UInt8

Equations

• instOrOpUInt8 = { or := UInt8.lor }

instance instXorUInt8 : Xor UInt8

Equations

• instXorUInt8 = { xor := UInt8.xor }

instance instShiftLeftUInt8 : ShiftLeft UInt8

Equations

• instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }

instance instShiftRightUInt8 : ShiftRight UInt8

Equations

• instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }

@[extern lean_bool_to_uint8]

def Bool.toUInt8 (b : Bool) : UInt8

Converts true to 1 and false to 0.

Equations

• b.toUInt8 = if b = true then 1 else 0

@[extern lean_uint8_dec_lt]

def UInt8.decLt (a b : UInt8) : Decidable (a < b)

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

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_uint8_dec_le]

def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b)

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

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

instance instDecidableLtUInt8 (a b : UInt8) : Decidable (a < b)

Equations

• instDecidableLtUInt8 a b = a.decLt b

instance instDecidableLeUInt8 (a b : UInt8) : Decidable (a ≤ b)

Equations

• instDecidableLeUInt8 a b = a.decLe b

instance instMaxUInt8 : Max UInt8

Equations

• instMaxUInt8 = maxOfLe

instance instMinUInt8 : Min UInt8

Equations

• instMinUInt8 = minOfLe

@[inline]

def UInt16.ofFin (a : Fin size) : UInt16

Converts a Fin UInt16.size into the corresponding UInt16.

Equations

• UInt16.ofFin a = { toBitVec := { toFin := a } }

@[deprecated UInt16.ofBitVec (since := "2025-02-12")]

def UInt16.mk (bitVec : BitVec 16) : UInt16

Creates a UInt16 from a BitVec 16. This function is overridden with a native implementation.

Equations

• UInt16.mk bitVec = { toBitVec := bitVec }

@[inline, deprecated UInt16.ofNatLT (since := "2025-02-13")]

def UInt16.ofNatCore (n : Nat) (h : n < size) : UInt16

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

This function is overridden at runtime with an efficient implementation.

Equations

• UInt16.ofNatCore n h = UInt16.ofNatLT n h

@[extern lean_uint16_add]

def UInt16.add (a b : UInt16) : UInt16

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.

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint16_sub]

def UInt16.sub (a b : UInt16) : UInt16

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.

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint16_mul]

def UInt16.mul (a b : UInt16) : UInt16

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.

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint16_div]

def UInt16.div (a b : UInt16) : UInt16

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.

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint16_mod]

def UInt16.mod (a b : UInt16) : UInt16

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

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt16.mod (since := "2024-09-23")]

def UInt16.modn (a : UInt16) (n : Nat) : UInt16

Equations

• a.modn n = { toBitVec := ↑↑(a.toFin.modn n) }

@[extern lean_uint16_land]

def UInt16.land (a b : UInt16) : UInt16

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.

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint16_lor]

def UInt16.lor (a b : UInt16) : UInt16

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.

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint16_xor]

def UInt16.xor (a b : UInt16) : UInt16

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.

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint16_shift_left]

def UInt16.shiftLeft (a b : UInt16) : UInt16

Bitwise left shift for 16-bit unsigned integers. Usually accessed via the <<< operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 16).toBitVec }

@[extern lean_uint16_shift_right]

def UInt16.shiftRight (a b : UInt16) : UInt16

Bitwise right shift for 16-bit unsigned integers. Usually accessed via the >>> operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 16).toBitVec }

def UInt16.lt (a b : UInt16) : Prop

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

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt16.le (a b : UInt16) : Prop

Non-strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt16 : Add UInt16

Equations

• instAddUInt16 = { add := UInt16.add }

instance instSubUInt16 : Sub UInt16

Equations

• instSubUInt16 = { sub := UInt16.sub }

instance instMulUInt16 : Mul UInt16

Equations

• instMulUInt16 = { mul := UInt16.mul }

instance instModUInt16 : Mod UInt16

Equations

• instModUInt16 = { mod := UInt16.mod }

instance instHModUInt16Nat : HMod UInt16 Nat UInt16

Equations

• instHModUInt16Nat = { hMod := UInt16.modn }

instance instDivUInt16 : Div UInt16

Equations

• instDivUInt16 = { div := UInt16.div }

instance instLTUInt16 : LT UInt16

Equations

• instLTUInt16 = { lt := UInt16.lt }

instance instLEUInt16 : LE UInt16

Equations

• instLEUInt16 = { le := UInt16.le }

@[extern lean_uint16_complement]

def UInt16.complement (a : UInt16) : UInt16

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.

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

@[extern lean_uint16_neg]

def UInt16.neg (a : UInt16) : UInt16

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.

Equations

• a.neg = { toBitVec := -a.toBitVec }

instance instComplementUInt16 : Complement UInt16

Equations

• instComplementUInt16 = { complement := UInt16.complement }

instance instNegUInt16 : Neg UInt16

Equations

• instNegUInt16 = { neg := UInt16.neg }

instance instAndOpUInt16 : AndOp UInt16

Equations

• instAndOpUInt16 = { and := UInt16.land }

instance instOrOpUInt16 : OrOp UInt16

Equations

• instOrOpUInt16 = { or := UInt16.lor }

instance instXorUInt16 : Xor UInt16

Equations

• instXorUInt16 = { xor := UInt16.xor }

instance instShiftLeftUInt16 : ShiftLeft UInt16

Equations

• instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }

instance instShiftRightUInt16 : ShiftRight UInt16

Equations

• instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }

@[extern lean_bool_to_uint16]

def Bool.toUInt16 (b : Bool) : UInt16

Converts true to 1 and false to 0.

Equations

• b.toUInt16 = if b = true then 1 else 0

@[extern lean_uint16_dec_lt]

def UInt16.decLt (a b : UInt16) : Decidable (a < b)

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

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_uint16_dec_le]

def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b)

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

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

instance instDecidableLtUInt16 (a b : UInt16) : Decidable (a < b)

Equations

• instDecidableLtUInt16 a b = a.decLt b

instance instDecidableLeUInt16 (a b : UInt16) : Decidable (a ≤ b)

Equations

• instDecidableLeUInt16 a b = a.decLe b

instance instMaxUInt16 : Max UInt16

Equations

• instMaxUInt16 = maxOfLe

instance instMinUInt16 : Min UInt16

Equations

• instMinUInt16 = minOfLe

@[inline]

def UInt32.ofFin (a : Fin size) : UInt32

Converts a Fin UInt32.size into the corresponding UInt32.

Equations

• UInt32.ofFin a = { toBitVec := { toFin := a } }

@[deprecated UInt32.ofBitVec (since := "2025-02-12")]

def UInt32.mk (bitVec : BitVec 32) : UInt32

Creates a UInt32 from a BitVec 32. This function is overridden with a native implementation.

Equations

• UInt32.mk bitVec = { toBitVec := bitVec }

@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13")]

def UInt32.ofNatCore (n : Nat) (h : n < size) : UInt32

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

• UInt32.ofNatCore n h = UInt32.ofNatLT n h

@[extern lean_uint32_add]

def UInt32.add (a b : UInt32) : UInt32

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.

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint32_sub]

def UInt32.sub (a b : UInt32) : UInt32

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.

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint32_mul]

def UInt32.mul (a b : UInt32) : UInt32

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.

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint32_div]

def UInt32.div (a b : UInt32) : UInt32

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.

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint32_mod]

def UInt32.mod (a b : UInt32) : UInt32

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

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt32.mod (since := "2024-09-23")]

def UInt32.modn (a : UInt32) (n : Nat) : UInt32

Equations

• a.modn n = { toBitVec := ↑↑(a.toFin.modn n) }

@[extern lean_uint32_land]

def UInt32.land (a b : UInt32) : UInt32

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.

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint32_lor]

def UInt32.lor (a b : UInt32) : UInt32

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.

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint32_xor]

def UInt32.xor (a b : UInt32) : UInt32

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.

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint32_shift_left]

def UInt32.shiftLeft (a b : UInt32) : UInt32

Bitwise left shift for 32-bit unsigned integers. Usually accessed via the <<< operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 32).toBitVec }

@[extern lean_uint32_shift_right]

def UInt32.shiftRight (a b : UInt32) : UInt32

Bitwise right shift for 32-bit unsigned integers. Usually accessed via the >>> operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 32).toBitVec }

def UInt32.lt (a b : UInt32) : Prop

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

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt32.le (a b : UInt32) : Prop

Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt32 : Add UInt32

Equations

• instAddUInt32 = { add := UInt32.add }

instance instSubUInt32 : Sub UInt32

Equations

• instSubUInt32 = { sub := UInt32.sub }

instance instMulUInt32 : Mul UInt32

Equations

• instMulUInt32 = { mul := UInt32.mul }

instance instModUInt32 : Mod UInt32

Equations

• instModUInt32 = { mod := UInt32.mod }

instance instHModUInt32Nat : HMod UInt32 Nat UInt32

Equations

• instHModUInt32Nat = { hMod := UInt32.modn }

instance instDivUInt32 : Div UInt32

Equations

• instDivUInt32 = { div := UInt32.div }

instance instLTUInt32_1 : LT UInt32

Equations

• instLTUInt32_1 = { lt := UInt32.lt }

instance instLEUInt32_1 : LE UInt32

Equations

• instLEUInt32_1 = { le := UInt32.le }

@[extern lean_uint32_complement]

def UInt32.complement (a : UInt32) : UInt32

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.

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

@[extern lean_uint32_neg]

def UInt32.neg (a : UInt32) : UInt32

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.

Equations

• a.neg = { toBitVec := -a.toBitVec }

instance instComplementUInt32 : Complement UInt32

Equations

• instComplementUInt32 = { complement := UInt32.complement }

instance instNegUInt32 : Neg UInt32

Equations

• instNegUInt32 = { neg := UInt32.neg }

instance instAndOpUInt32 : AndOp UInt32

Equations

• instAndOpUInt32 = { and := UInt32.land }

instance instOrOpUInt32 : OrOp UInt32

Equations

• instOrOpUInt32 = { or := UInt32.lor }

instance instXorUInt32 : Xor UInt32

Equations

• instXorUInt32 = { xor := UInt32.xor }

instance instShiftLeftUInt32 : ShiftLeft UInt32

Equations

• instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }

instance instShiftRightUInt32 : ShiftRight UInt32

Equations

• instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }

@[extern lean_bool_to_uint32]

def Bool.toUInt32 (b : Bool) : UInt32

Converts true to 1 and false to 0.

Equations

• b.toUInt32 = if b = true then 1 else 0

@[inline]

def UInt64.ofFin (a : Fin size) : UInt64

Converts a Fin UInt64.size into the corresponding UInt64.

Equations

• UInt64.ofFin a = { toBitVec := { toFin := a } }

@[deprecated UInt64.ofBitVec (since := "2025-02-12")]

def UInt64.mk (bitVec : BitVec 64) : UInt64

Creates a UInt64 from a BitVec 64. This function is overridden with a native implementation.

Equations

• UInt64.mk bitVec = { toBitVec := bitVec }

@[inline, deprecated UInt64.ofNatLT (since := "2025-02-13")]

def UInt64.ofNatCore (n : Nat) (h : n < size) : UInt64

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

This function is overridden at runtime with an efficient implementation.

Equations

• UInt64.ofNatCore n h = UInt64.ofNatLT n h

@[extern lean_uint64_add]

def UInt64.add (a b : UInt64) : UInt64

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.

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_uint64_sub]

def UInt64.sub (a b : UInt64) : UInt64

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.

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

@[extern lean_uint64_mul]

def UInt64.mul (a b : UInt64) : UInt64

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.

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_uint64_div]

def UInt64.div (a b : UInt64) : UInt64

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.

Equations

• a.div b = { toBitVec := a.toBitVec.udiv b.toBitVec }

@[extern lean_uint64_mod]

def UInt64.mod (a b : UInt64) : UInt64

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

Equations

• a.mod b = { toBitVec := a.toBitVec.umod b.toBitVec }

@[deprecated UInt64.mod (since := "2024-09-23")]

def UInt64.modn (a : UInt64) (n : Nat) : UInt64

Equations

• a.modn n = { toBitVec := ↑↑(a.toFin.modn n) }

@[extern lean_uint64_land]

def UInt64.land (a b : UInt64) : UInt64

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.

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_uint64_lor]

def UInt64.lor (a b : UInt64) : UInt64

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.

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_uint64_xor]

def UInt64.xor (a b : UInt64) : UInt64

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.

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_uint64_shift_left]

def UInt64.shiftLeft (a b : UInt64) : UInt64

Bitwise left shift for 64-bit unsigned integers. Usually accessed via the <<< operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod 64).toBitVec }

@[extern lean_uint64_shift_right]

def UInt64.shiftRight (a b : UInt64) : UInt64

Bitwise right shift for 64-bit unsigned integers. Usually accessed via the >>> operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod 64).toBitVec }

def UInt64.lt (a b : UInt64) : Prop

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

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def UInt64.le (a b : UInt64) : Prop

Non-strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance instAddUInt64 : Add UInt64

Equations

• instAddUInt64 = { add := UInt64.add }

instance instSubUInt64 : Sub UInt64

Equations

• instSubUInt64 = { sub := UInt64.sub }

instance instMulUInt64 : Mul UInt64

Equations

• instMulUInt64 = { mul := UInt64.mul }

instance instModUInt64 : Mod UInt64

Equations

• instModUInt64 = { mod := UInt64.mod }

instance instHModUInt64Nat : HMod UInt64 Nat UInt64

Equations

• instHModUInt64Nat = { hMod := UInt64.modn }

instance instDivUInt64 : Div UInt64

Equations

• instDivUInt64 = { div := UInt64.div }

instance instLTUInt64 : LT UInt64

Equations

• instLTUInt64 = { lt := UInt64.lt }

instance instLEUInt64 : LE UInt64

Equations

• instLEUInt64 = { le := UInt64.le }

@[extern lean_uint64_complement]

def UInt64.complement (a : UInt64) : UInt64

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.

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

@[extern lean_uint64_neg]

def UInt64.neg (a : UInt64) : UInt64

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.

Equations

• a.neg = { toBitVec := -a.toBitVec }

instance instComplementUInt64 : Complement UInt64

Equations

• instComplementUInt64 = { complement := UInt64.complement }

instance instNegUInt64 : Neg UInt64

Equations

• instNegUInt64 = { neg := UInt64.neg }

instance instAndOpUInt64 : AndOp UInt64

Equations

• instAndOpUInt64 = { and := UInt64.land }

instance instOrOpUInt64 : OrOp UInt64

Equations

• instOrOpUInt64 = { or := UInt64.lor }

instance instXorUInt64 : Xor UInt64

Equations

• instXorUInt64 = { xor := UInt64.xor }

instance instShiftLeftUInt64 : ShiftLeft UInt64

Equations

• instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }

instance instShiftRightUInt64 : ShiftRight UInt64

Equations

• instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }

@[extern lean_bool_to_uint64]

def Bool.toUInt64 (b : Bool) : UInt64

Converts true to 1 and false to 0.

Equations

• b.toUInt64 = if b = true then 1 else 0

@[extern lean_uint64_dec_lt]

def UInt64.decLt (a b : UInt64) : Decidable (a < b)

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

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_uint64_dec_le]

def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b)

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

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

instance instDecidableLtUInt64 (a b : UInt64) : Decidable (a < b)

Equations

• instDecidableLtUInt64 a b = a.decLt b

instance instDecidableLeUInt64 (a b : UInt64) : Decidable (a ≤ b)

Equations

• instDecidableLeUInt64 a b = a.decLe b

instance instMaxUInt64 : Max UInt64

Equations

• instMaxUInt64 = maxOfLe

instance instMinUInt64 : Min UInt64

Equations

• instMinUInt64 = minOfLe

@[inline]

def USize.ofFin (a : Fin size) : USize

Converts a Fin USize.size into the corresponding USize.

Equations

• USize.ofFin a = { toBitVec := { toFin := a } }

@[deprecated USize.ofBitVec (since := "2025-02-12")]

def USize.mk (bitVec : BitVec System.Platform.numBits) : USize

Creates a USize from a BitVec System.Platform.numBits. This function is overridden with a native implementation.

Equations

• USize.mk bitVec = { toBitVec := bitVec }

@[inline, deprecated USize.ofNatLT (since := "2025-02-13")]

def USize.ofNatCore (n : Nat) (h : n < size) : USize

Converts a natural number to a USize. Requires a proof that the number is small enough to be representable without overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• USize.ofNatCore n h = USize.ofNatLT n h

@[simp]

theorem USize.le_size : 2 ^ 32 ≤ size

@[simp]

theorem USize.size_le : size ≤ 2 ^ 64

@[deprecated USize.size_le (since := "2025-02-24")]

theorem usize_size_le : USize.size ≤ 18446744073709551616

@[deprecated USize.le_size (since := "2025-02-24")]

theorem le_usize_size : 4294967296 ≤ USize.size

@[extern lean_usize_mul]

def USize.mul (a b : USize) : USize

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.

Equations

• a.mul b = { toBitVec := a.toBitVec * b.toBitVec }

@[extern lean_usize_div]

def USize.div (a b : USize) : USize

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.

Equations

• a.div b = { toBitVec := a.toBitVec / b.toBitVec }

@[extern lean_usize_mod]

def USize.mod (a b : USize) : USize

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

Equations

• a.mod b = { toBitVec := a.toBitVec % b.toBitVec }

@[deprecated USize.mod (since := "2024-09-23")]

def USize.modn (a : USize) (n : Nat) : USize

Equations

• a.modn n = { toBitVec := ↑↑(a.toFin.modn n) }

@[extern lean_usize_land]

def USize.land (a b : USize) : USize

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.

Equations

• a.land b = { toBitVec := a.toBitVec &&& b.toBitVec }

@[extern lean_usize_lor]

def USize.lor (a b : USize) : USize

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.

Equations

• a.lor b = { toBitVec := a.toBitVec ||| b.toBitVec }

@[extern lean_usize_xor]

def USize.xor (a b : USize) : USize

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.

Equations

• a.xor b = { toBitVec := a.toBitVec ^^^ b.toBitVec }

@[extern lean_usize_shift_left]

def USize.shiftLeft (a b : USize) : USize

Bitwise left shift for word-sized unsigned integers. Usually accessed via the <<< operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toBitVec := a.toBitVec <<< (b.mod (USize.ofNat System.Platform.numBits)).toBitVec }

@[extern lean_usize_shift_right]

def USize.shiftRight (a b : USize) : USize

Bitwise right shift for word-sized unsigned integers. Usually accessed via the >>> operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toBitVec := a.toBitVec >>> (b.mod (USize.ofNat System.Platform.numBits)).toBitVec }

@[extern lean_usize_of_nat]

def USize.ofNat32 (n : Nat) (h : n < 4294967296) : USize

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.

Equations

• USize.ofNat32 n h = USize.ofNatLT n ⋯

@[extern lean_uint8_to_usize]

def UInt8.toUSize (a : UInt8) : USize

Converts 8-bit unsigned integers to word-sized unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯

@[extern lean_usize_to_uint8]

def USize.toUInt8 (a : USize) : UInt8

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

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint16_to_usize]

def UInt16.toUSize (a : UInt16) : USize

Converts 16-bit unsigned integers to word-sized unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯

@[extern lean_usize_to_uint16]

def USize.toUInt16 (a : USize) : UInt16

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

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint32_to_usize]

def UInt32.toUSize (a : UInt32) : USize

Converts 32-bit unsigned integers to word-sized unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUSize = USize.ofNat32 a.toBitVec.toNat ⋯

@[extern lean_usize_to_uint32]

def USize.toUInt32 (a : USize) : UInt32

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.

Equations

• a.toUInt32 = a.toNat.toUInt32

@[extern lean_uint64_to_usize]

def UInt64.toUSize (a : UInt64) : USize

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.

Equations

• a.toUSize = a.toNat.toUSize

@[extern lean_usize_to_uint64]

def USize.toUInt64 (a : USize) : UInt64

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.

Equations

• a.toUInt64 = UInt64.ofNatLT a.toBitVec.toNat ⋯

instance instMulUSize : Mul USize

Equations

• instMulUSize = { mul := USize.mul }

instance instModUSize : Mod USize

Equations

• instModUSize = { mod := USize.mod }

instance instHModUSizeNat : HMod USize Nat USize

Equations

• instHModUSizeNat = { hMod := USize.modn }

instance instDivUSize : Div USize

Equations

• instDivUSize = { div := USize.div }

@[extern lean_usize_complement]

def USize.complement (a : USize) : USize

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.

Equations

• a.complement = { toBitVec := ~~~a.toBitVec }

@[extern lean_usize_neg]

def USize.neg (a : USize) : USize

Negation of word-sized unsigned integers, computed modulo USize.size.

This function is overridden at runtime with an efficient implementation.

Equations

• a.neg = { toBitVec := -a.toBitVec }

instance instComplementUSize : Complement USize

Equations

• instComplementUSize = { complement := USize.complement }

instance instNegUSize : Neg USize

Equations

• instNegUSize = { neg := USize.neg }

instance instAndOpUSize : AndOp USize

Equations

• instAndOpUSize = { and := USize.land }

instance instOrOpUSize : OrOp USize

Equations

• instOrOpUSize = { or := USize.lor }

instance instXorUSize : Xor USize

Equations

• instXorUSize = { xor := USize.xor }

instance instShiftLeftUSize : ShiftLeft USize

Equations

• instShiftLeftUSize = { shiftLeft := USize.shiftLeft }

instance instShiftRightUSize : ShiftRight USize

Equations

• instShiftRightUSize = { shiftRight := USize.shiftRight }

@[extern lean_bool_to_usize]

def Bool.toUSize (b : Bool) : USize

Converts true to 1 and false to 0.

Equations

• b.toUSize = if b = true then 1 else 0

instance instMaxUSize : Max USize

Equations

• instMaxUSize = maxOfLe

instance instMinUSize : Min USize

Equations

• instMinUSize = minOfLe