source
@[inline]
def UInt8.ofFin (a : Fin size) :
UInt8

Converts a `Fin UInt8.size` into the corresponding `UInt8`.

Equations

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

Instances For

source
def UInt8.ofInt (x : Int) :
UInt8

Converts an `Int` to a `UInt8` by taking the (non-negative remainder of the division by `2 ^ 8`.

Equations

- UInt8.ofInt x = UInt8.ofNat (x % 2 ^ 8).toNat

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
def UInt8.pow (x : UInt8) (n : Nat) :
UInt8

The power operation, raising an 8-bit unsigned integer to a natural number power, wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently not overridden at runtime with an efficient implementation, and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.

Equations

- x.pow 0 = 1
- x.pow n_2.succ = (x.pow n_2).mul x

Instances For

source
@[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 }

Instances For

source
@[deprecated UInt8.mod (since := "2024-09-23")]
def UInt8.modn (a : UInt8) (n : Nat) :
UInt8
Equations

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
instance instAddUInt8 :
Add UInt8
Equations

- instAddUInt8 = { add := UInt8.add }

source
instance instSubUInt8 :
Sub UInt8
Equations

- instSubUInt8 = { sub := UInt8.sub }

source
instance instMulUInt8 :
Mul UInt8
Equations

- instMulUInt8 = { mul := UInt8.mul }

source
instance instPowUInt8Nat :
Pow UInt8 Nat
Equations

- instPowUInt8Nat = { pow := UInt8.pow }

source
instance instModUInt8 :
Mod UInt8
Equations

- instModUInt8 = { mod := UInt8.mod }

source
instance instHModUInt8Nat :
HMod UInt8 Nat UInt8
Equations

- instHModUInt8Nat = { hMod := UInt8.modn }

source
instance instDivUInt8 :
Div UInt8
Equations

- instDivUInt8 = { div := UInt8.div }

source
@[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 }

Instances For

source
@[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 }

Instances For

source
instance instComplementUInt8 :
Complement UInt8
Equations

- instComplementUInt8 = { complement := UInt8.complement }

source
instance instNegUInt8 :
Neg UInt8
Equations

- instNegUInt8 = { neg := UInt8.neg }

source
instance instAndOpUInt8 :
AndOp UInt8
Equations

- instAndOpUInt8 = { and := UInt8.land }

source
instance instOrOpUInt8 :
OrOp UInt8
Equations

- instOrOpUInt8 = { or := UInt8.lor }

source
instance instXorOpUInt8 :
XorOp UInt8
Equations

- instXorOpUInt8 = { xor := UInt8.xor }

source
instance instShiftLeftUInt8 :
ShiftLeft UInt8
Equations

- instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }

source
instance instShiftRightUInt8 :
ShiftRight UInt8
Equations

- instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }

source
@[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

Instances For

source
instance instMaxUInt8 :
Max UInt8
Equations

- instMaxUInt8 = maxOfLe

source
instance instMinUInt8 :
Min UInt8
Equations

- instMinUInt8 = minOfLe

source
@[inline]
def UInt8.toAsciiLower (b : UInt8) :
UInt8

If `b` is the ASCII value of an uppercase character return the corresponding lowercase value, otherwise leave it untouched.

Equations

- b.toAsciiLower = if (decide (b ≥ 65) && decide (b ≤ 90)) = true then b + 32 else b

Instances For

source
@[inline]
def UInt16.ofFin (a : Fin size) :
UInt16

Converts a `Fin UInt16.size` into the corresponding `UInt16`.

Equations

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

Instances For

source
def UInt16.ofInt (x : Int) :
UInt16

Converts an `Int` to a `UInt16` by taking the (non-negative remainder of the division by `2 ^ 16`.

Equations

- UInt16.ofInt x = UInt16.ofNat (x % 2 ^ 16).toNat

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
def UInt16.pow (x : UInt16) (n : Nat) :
UInt16

The power operation, raising a 16-bit unsigned integer to a natural number power, wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently not overridden at runtime with an efficient implementation, and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.

Equations

- x.pow 0 = 1
- x.pow n_2.succ = (x.pow n_2).mul x

Instances For

source
@[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 }

Instances For

source
@[deprecated UInt16.mod (since := "2024-09-23")]
def UInt16.modn (a : UInt16) (n : Nat) :
UInt16
Equations

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[extern lean_uint16_xor]
def UInt16.xor (a b : UInt16) :
UInt16

Bitwise exclusive or for 16-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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
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)

Instances For

source
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)

Instances For

source
instance instAddUInt16 :
Add UInt16
Equations

- instAddUInt16 = { add := UInt16.add }

source
instance instSubUInt16 :
Sub UInt16
Equations

- instSubUInt16 = { sub := UInt16.sub }

source
instance instMulUInt16 :
Mul UInt16
Equations

- instMulUInt16 = { mul := UInt16.mul }

source
instance instPowUInt16Nat :
Pow UInt16 Nat
Equations

- instPowUInt16Nat = { pow := UInt16.pow }

source
instance instModUInt16 :
Mod UInt16
Equations

- instModUInt16 = { mod := UInt16.mod }

source
instance instHModUInt16Nat :
HMod UInt16 Nat UInt16
Equations

- instHModUInt16Nat = { hMod := UInt16.modn }

source
instance instDivUInt16 :
Div UInt16
Equations

- instDivUInt16 = { div := UInt16.div }

source
instance instLTUInt16 :
LT UInt16
Equations

- instLTUInt16 = { lt := UInt16.lt }

source
instance instLEUInt16 :
LE UInt16
Equations

- instLEUInt16 = { le := UInt16.le }

source
@[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 }

Instances For

source
@[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 }

Instances For

source
instance instComplementUInt16 :
Complement UInt16
Equations

- instComplementUInt16 = { complement := UInt16.complement }

source
instance instNegUInt16 :
Neg UInt16
Equations

- instNegUInt16 = { neg := UInt16.neg }

source
instance instAndOpUInt16 :
AndOp UInt16
Equations

- instAndOpUInt16 = { and := UInt16.land }

source
instance instOrOpUInt16 :
OrOp UInt16
Equations

- instOrOpUInt16 = { or := UInt16.lor }

source
instance instXorOpUInt16 :
XorOp UInt16
Equations

- instXorOpUInt16 = { xor := UInt16.xor }

source
instance instShiftLeftUInt16 :
ShiftLeft UInt16
Equations

- instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }

source
instance instShiftRightUInt16 :
ShiftRight UInt16
Equations

- instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }

source
@[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

Instances For

source
@[extern lean_uint16_dec_lt]
instance 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))

source
@[extern lean_uint16_dec_le]
instance 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))

source
instance instMaxUInt16 :
Max UInt16
Equations

- instMaxUInt16 = maxOfLe

source
instance instMinUInt16 :
Min UInt16
Equations

- instMinUInt16 = minOfLe

source
@[inline]
def UInt32.ofFin (a : Fin size) :
UInt32

Converts a `Fin UInt32.size` into the corresponding `UInt32`.

Equations

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

Instances For

source
def UInt32.ofInt (x : Int) :
UInt32

Converts an `Int` to a `UInt32` by taking the (non-negative remainder of the division by `2 ^ 32`.

Equations

- UInt32.ofInt x = UInt32.ofNat (x % 2 ^ 32).toNat

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
def UInt32.pow (x : UInt32) (n : Nat) :
UInt32

The power operation, raising a 32-bit unsigned integer to a natural number power, wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently not overridden at runtime with an efficient implementation, and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.

Equations

- x.pow 0 = 1
- x.pow n_2.succ = (x.pow n_2).mul x

Instances For

source
@[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 }

Instances For

source
@[deprecated UInt32.mod (since := "2024-09-23")]
def UInt32.modn (a : UInt32) (n : Nat) :
UInt32
Equations

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
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)

Instances For

source
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)

Instances For

source
instance instAddUInt32 :
Add UInt32
Equations

- instAddUInt32 = { add := UInt32.add }

source
instance instSubUInt32 :
Sub UInt32
Equations

- instSubUInt32 = { sub := UInt32.sub }

source
instance instMulUInt32 :
Mul UInt32
Equations

- instMulUInt32 = { mul := UInt32.mul }

source
instance instPowUInt32Nat :
Pow UInt32 Nat
Equations

- instPowUInt32Nat = { pow := UInt32.pow }

source
instance instModUInt32 :
Mod UInt32
Equations

- instModUInt32 = { mod := UInt32.mod }

source
instance instHModUInt32Nat :
HMod UInt32 Nat UInt32
Equations

- instHModUInt32Nat = { hMod := UInt32.modn }

source
instance instDivUInt32 :
Div UInt32
Equations

- instDivUInt32 = { div := UInt32.div }

source
@[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 }

Instances For

source
@[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 }

Instances For

source
instance instComplementUInt32 :
Complement UInt32
Equations

- instComplementUInt32 = { complement := UInt32.complement }

source
instance instNegUInt32 :
Neg UInt32
Equations

- instNegUInt32 = { neg := UInt32.neg }

source
instance instAndOpUInt32 :
AndOp UInt32
Equations

- instAndOpUInt32 = { and := UInt32.land }

source
instance instOrOpUInt32 :
OrOp UInt32
Equations

- instOrOpUInt32 = { or := UInt32.lor }

source
instance instXorOpUInt32 :
XorOp UInt32
Equations

- instXorOpUInt32 = { xor := UInt32.xor }

source
instance instShiftLeftUInt32 :
ShiftLeft UInt32
Equations

- instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }

source
instance instShiftRightUInt32 :
ShiftRight UInt32
Equations

- instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }

source
@[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

Instances For

source
@[inline]
def UInt64.ofFin (a : Fin size) :
UInt64

Converts a `Fin UInt64.size` into the corresponding `UInt64`.

Equations

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

Instances For

source
def UInt64.ofInt (x : Int) :
UInt64

Converts an `Int` to a `UInt64` by taking the (non-negative remainder of the division by `2 ^ 64`.

Equations

- UInt64.ofInt x = UInt64.ofNat (x % 2 ^ 64).toNat

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
def UInt64.pow (x : UInt64) (n : Nat) :
UInt64

The power operation, raising a 64-bit unsigned integer to a natural number power, wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently not overridden at runtime with an efficient implementation, and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.

Equations

- x.pow 0 = 1
- x.pow n_2.succ = (x.pow n_2).mul x

Instances For

source
@[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 }

Instances For

source
@[deprecated UInt64.mod (since := "2024-09-23")]
def UInt64.modn (a : UInt64) (n : Nat) :
UInt64
Equations

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
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)

Instances For

source
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)

Instances For

source
instance instAddUInt64 :
Add UInt64
Equations

- instAddUInt64 = { add := UInt64.add }

source
instance instSubUInt64 :
Sub UInt64
Equations

- instSubUInt64 = { sub := UInt64.sub }

source
instance instMulUInt64 :
Mul UInt64
Equations

- instMulUInt64 = { mul := UInt64.mul }

source
instance instPowUInt64Nat :
Pow UInt64 Nat
Equations

- instPowUInt64Nat = { pow := UInt64.pow }

source
instance instModUInt64 :
Mod UInt64
Equations

- instModUInt64 = { mod := UInt64.mod }

source
instance instHModUInt64Nat :
HMod UInt64 Nat UInt64
Equations

- instHModUInt64Nat = { hMod := UInt64.modn }

source
instance instDivUInt64 :
Div UInt64
Equations

- instDivUInt64 = { div := UInt64.div }

source
instance instLTUInt64 :
LT UInt64
Equations

- instLTUInt64 = { lt := UInt64.lt }

source
instance instLEUInt64 :
LE UInt64
Equations

- instLEUInt64 = { le := UInt64.le }

source
@[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 }

Instances For

source
@[extern lean_uint64_neg]
def UInt64.neg (a : UInt64) :
UInt64

Negation of 64-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 }

Instances For

source
instance instComplementUInt64 :
Complement UInt64
Equations

- instComplementUInt64 = { complement := UInt64.complement }

source
instance instNegUInt64 :
Neg UInt64
Equations

- instNegUInt64 = { neg := UInt64.neg }

source
instance instAndOpUInt64 :
AndOp UInt64
Equations

- instAndOpUInt64 = { and := UInt64.land }

source
instance instOrOpUInt64 :
OrOp UInt64
Equations

- instOrOpUInt64 = { or := UInt64.lor }

source
instance instXorOpUInt64 :
XorOp UInt64
Equations

- instXorOpUInt64 = { xor := UInt64.xor }

source
instance instShiftLeftUInt64 :
ShiftLeft UInt64
Equations

- instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }

source
instance instShiftRightUInt64 :
ShiftRight UInt64
Equations

- instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }

source
@[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

Instances For

source
@[extern lean_uint64_dec_lt]
instance 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))

source
@[extern lean_uint64_dec_le]
instance 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))

source
instance instMaxUInt64 :
Max UInt64
Equations

- instMaxUInt64 = maxOfLe

source
instance instMinUInt64 :
Min UInt64
Equations

- instMinUInt64 = minOfLe

source
@[inline]
def USize.ofFin (a : Fin size) :
USize

Converts a `Fin USize.size` into the corresponding `USize`.

Equations

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

Instances For

source
def USize.ofInt (x : Int) :
USize

Converts an `Int` to a `USize` by taking the (non-negative remainder of the division by `2 ^ numBits`.

Equations

- USize.ofInt x = USize.ofNat (x % 2 ^ System.Platform.numBits).toNat

Instances For

source
@[simp]
theorem USize.le_size :
2 ^ 32 ≤ size
source
@[simp]
theorem USize.size_le :
size ≤ 2 ^ 64
source
@[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 }

Instances For

source
@[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 }

Instances For

source
def USize.pow (x : USize) (n : Nat) :
USize

The power operation, raising a word-sized unsigned integer to a natural number power, wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently not overridden at runtime with an efficient implementation, and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.

Equations

- x.pow 0 = 1
- x.pow n_2.succ = (x.pow n_2).mul x

Instances For

source
@[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 }

Instances For

source
@[deprecated USize.mod (since := "2024-09-23")]
def USize.modn (a : USize) (n : Nat) :
USize
Equations

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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[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 ⋯

Instances For

source
@[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 ⋯

Instances For

source
@[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

Instances For

source
@[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 ⋯

Instances For

source
@[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

Instances For

source
@[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 ⋯

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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 ⋯

Instances For

source
instance instMulUSize :
Mul USize
Equations

- instMulUSize = { mul := USize.mul }

source
instance instPowUSizeNat :
Pow USize Nat
Equations

- instPowUSizeNat = { pow := USize.pow }

source
instance instModUSize :
Mod USize
Equations

- instModUSize = { mod := USize.mod }

source
instance instHModUSizeNat :
HMod USize Nat USize
Equations

- instHModUSizeNat = { hMod := USize.modn }

source
instance instDivUSize :
Div USize
Equations

- instDivUSize = { div := USize.div }

source
@[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 }

Instances For

source
@[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 }

Instances For

source
instance instComplementUSize :
Complement USize
Equations

- instComplementUSize = { complement := USize.complement }

source
instance instNegUSize :
Neg USize
Equations

- instNegUSize = { neg := USize.neg }

source
instance instAndOpUSize :
AndOp USize
Equations

- instAndOpUSize = { and := USize.land }

source
instance instOrOpUSize :
OrOp USize
Equations

- instOrOpUSize = { or := USize.lor }

source
instance instXorOpUSize :
XorOp USize
Equations

- instXorOpUSize = { xor := USize.xor }

source
instance instShiftLeftUSize :
ShiftLeft USize
Equations

- instShiftLeftUSize = { shiftLeft := USize.shiftLeft }

source
instance instShiftRightUSize :
ShiftRight USize
Equations

- instShiftRightUSize = { shiftRight := USize.shiftRight }

source
@[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

Instances For

source
instance instMaxUSize :
Max USize
Equations

- instMaxUSize = maxOfLe

source
instance instMinUSize :
Min USize
Equations

- instMinUSize = minOfLe