Lean's standard library includes the usual assortment of fixed-width integer types. From the perspective of formalization and proofs, these types are wrappers around bitvectors of the appropriate size; the wrappers ensure that the correct implementations of e.g. arithmetic operations are applied. In compiled code, they are represented efficiently: the compiler has special support for them, as it does for other fundamental types.
Fixed-width integers may be unsigned or signed.
Furthermore, they are available in five sizes: 8, 16, 32, and 64 bits, along with the current architecture's word size.
In their logical models, the unsigned integers are structures that wrap a BitVec of the appropriate width.
Signed integers wrap the corresponding unsigned integers, and use a twos-complement representation.
Unsigned integers that are the size of a word on the platform's architecture.
On a 32-bit architecture, USize is equivalent to UInt32. On a 64-bit machine, it is equivalent
to UInt64.
Constructor
USize.ofBitVec
Creates a USize from a BitVec System.Platform.numBits. This function is overridden with a
native implementation.
Fields
toBitVec : BitVec System.Platform.numBits
Unpacks a USize into a BitVec System.Platform.numBits. This function is overridden with a native
implementation.
Unsigned 8-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 8-bit value
rather than wrapping a BitVec 8.
Constructor
UInt8.ofBitVec
Unsigned 16-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 16-bit value
rather than wrapping a BitVec 16.
Constructor
UInt16.ofBitVec
Unsigned 32-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 32-bit value
rather than wrapping a BitVec 32.
Constructor
UInt32.ofBitVec
Unsigned 64-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 64-bit value
rather than wrapping a BitVec 64.
Constructor
UInt64.ofBitVec
Signed integers that are the size of a word on the platform's architecture.
On a 32-bit architecture, ISize is equivalent to Int32. On a 64-bit machine, it is equivalent to
Int64. This type has special support in the compiler so it can be represented by an unboxed value.
Constructor
ISize.ofUSize
Fields
toUSize : USize
Converts a word-sized signed integer into the word-sized unsigned integer that is its two's complement encoding.
Signed 8-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 8-bit value.
Constructor
Int8.ofUInt8
Fields
toUInt8 : UInt8
Converts an 8-bit signed integer into the 8-bit unsigned integer that is its two's complement encoding.
Signed 16-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 16-bit value.
Constructor
Int16.ofUInt16
Fields
toUInt16 : UInt16
Converts an 16-bit signed integer into the 16-bit unsigned integer that is its two's complement encoding.
Signed 32-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 32-bit value.
Constructor
Int32.ofUInt32
Fields
toUInt32 : UInt32
Converts an 32-bit signed integer into the 32-bit unsigned integer that is its two's complement encoding.
Signed 64-bit integers.
This type has special support in the compiler so it can be represented by an unboxed 64-bit value.
Constructor
Int64.ofUInt64
Fields
toUInt64 : UInt64
Converts an 64-bit signed integer into the 64-bit unsigned integer that is its two's complement encoding.
In compiled code in contexts that require boxed representations, fixed-width integer types that fit in one less bit than the platform's pointer size are always represented without additional allocations or indirections.
This always includes Int8, UInt8, Int16, and UInt16.
On 64-bit architectures, Int32 and UInt32 are also represented without pointers.
On 32-bit architectures, Int32 and UInt32 require a pointer to an object on the heap.
ISize, USize, Int64 and UInt64 may require pointers on all architectures.
Even though some fixed-with integer types require boxing in general, the compiler is able to represent them without boxing or pointer indirections in code paths that use only a specific fixed-width type rather than being polymorphic, potentially after a specialization pass.
This applies in most practical situations where these types are used: their values are represented using the corresponding unsigned fixed-width C type when a constructor parameter, function parameter, function return value, or intermediate result is known to be a fixed-width integer type.
The Lean run-time system includes primitives for storing fixed-width integers in constructors of inductive types, and the primitive operations are defined on the corresponding C types, so boxing tends to happen at the “edges” of integer calculations rather than for each intermediate result.
In contexts where other types might occur, such as the contents of polymorphic containers like Array, these types are boxed, even if an array is statically known to contain only a single fixed-width integer type.Marginal noteThe monomorphic array type ByteArray avoids boxing for arrays of UInt8.
Lean does not specialize the representation of inductive types or arrays.
Inspecting a function's type in Lean is not sufficient to determine how fixed-width integer values will be represented, because boxed values are not eagerly unboxed—a function that projects an Int64 from an array returns a boxed integer value.
All the fixed-width integer types have OfNat instances, which allow numerals to be used as literals, both in expression and in pattern contexts.
The signed types additionally have Neg instances, allowing negation to be applied.
Lean allows both decimal and hexadecimal literals to be used for types with OfNat instances.
In this example, literal notation is used to define masks.
structure Permissions where
readable : Bool
writable : Bool
executable : Bool
def Permissions.encode (p : Permissions) : UInt8 :=
let r := if p.readable then 0x01 else 0
let w := if p.writable then 0x02 else 0
let x := if p.executable then 0x04 else 0
r ||| w ||| x
def Permissions.decode (i : UInt8) : Permissions :=
⟨i &&& 0x01 ≠ 0, i &&& 0x02 ≠ 0, i &&& 0x04 ≠ 0⟩
Literals that overflow their types' precision are interpreted modulus the precision. Signed types, are interpreted according to the underlying twos-complement representation.
The following statements are all true:
example : (255 : UInt8) = 255 := ⊢ 255 = 255 All goals completed! 🐙
example : (256 : UInt8) = 0 := ⊢ 256 = 0 All goals completed! 🐙
example : (257 : UInt8) = 1 := ⊢ 257 = 1 All goals completed! 🐙
example : (0x7f : Int8) = 127 := ⊢ 127 = 127 All goals completed! 🐙
example : (0x8f : Int8) = -113 := ⊢ 143 = -113 All goals completed! 🐙
example : (0xff : Int8) = -1 := ⊢ 255 = -1 All goals completed! 🐙
Each fixed-width integer has a size, which is the number of distinct values that can be represented by the type.
This is not equivalent to C's sizeof operator, which instead determines how many bytes the type occupies.
IntConverts a word-sized signed integer to an arbitrary-precision integer that denotes the same number.
This function is overridden at runtime with an efficient implementation.
Converts an 8-bit signed integer to an arbitrary-precision integer that denotes the same number.
This function is overridden at runtime with an efficient implementation.
Converts a 16-bit signed integer to an arbitrary-precision integer that denotes the same number.
This function is overridden at runtime with an efficient implementation.
Converts a 32-bit signed integer to an arbitrary-precision integer that denotes the same number.
This function is overridden at runtime with an efficient implementation.
Converts a 64-bit signed integer to an arbitrary-precision integer that denotes the same number.
This function is overridden at runtime with an efficient implementation.
Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or underflow.
This function is overridden at runtime with an efficient implementation.
Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int8.ofInt 48 = 48
Int8.ofInt (-115) = -115
Int8.ofInt (-129) = 127
Int8.ofInt (128) = -128
Converts an arbitrary-precision integer to a 16-bit signed integer, wrapping on overflow or underflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int16.ofInt 48 = 48
Int16.ofInt (-129) = -129
Int16.ofInt (128) = 128
Int16.ofInt 70000 = 4464
Int16.ofInt (-40000) = 25536
Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int32.ofInt 48 = 48
Int32.ofInt (-129) = -129
Int32.ofInt 70000 = 70000
Int32.ofInt (-40000) = -40000
Int32.ofInt 2147483648 = -2147483648
Int32.ofInt (-2147483649) = 2147483647
Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int64.ofInt 48 = 48
Int64.ofInt (-40_000) = -40_000
Int64.ofInt 2_147_483_648 = 2_147_483_648
Int64.ofInt (-2_147_483_649) = -2_147_483_649
Int64.ofInt 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808
Int64.ofInt (-9_223_372_036_854_775_809) = 9_223_372_036_854_775_807
NatConverts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt8.ofNat 5 = 5
UInt8.ofNat 255 = 255
UInt8.ofNat 256 = 0
UInt8.ofNat 259 = 3
UInt8.ofNat 32770 = 2
Converts a natural number to an 8-bit signed integer, wrapping around on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int8.ofNat 53 = 53
Int8.ofNat 127 = 127
Int8.ofNat 128 = -128
Int8.ofNat 255 = -1
Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt16.ofNat 5 = 5
UInt16.ofNat 255 = 255
UInt16.ofNat 32770 = 32770
UInt16.ofNat 65537 = 1
Converts a natural number to a 16-bit signed integer, wrapping around on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int16.ofNat 127 = 127
Int16.ofNat 32767 = 32767
Int16.ofNat 32768 = -32768
Int16.ofNat 32770 = -32766
Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt32.ofNat 5 = 5
UInt32.ofNat 65539 = 65539
UInt32.ofNat 4_294_967_299 = 3
Converts a natural number to a 32-bit signed integer, wrapping around on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int32.ofNat 127 = 127
Int32.ofNat 32770 = 32770
Int32.ofNat 2_147_483_647 = 2_147_483_647
Int32.ofNat 2_147_483_648 = -2_147_483_648
Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt64.ofNat 5 = 5
UInt64.ofNat 65539 = 65539
UInt64.ofNat 4_294_967_299 = 4_294_967_299
UInt64.ofNat 18_446_744_073_709_551_620 = 4
Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
Int64.ofNat 127 = 127
Int64.ofNat 2_147_483_648 = 2_147_483_648
Int64.ofNat 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807
Int64.ofNat 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808
Int64.ofNat 18_446_744_073_709_551_618 = 0
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.
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.
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.
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.
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.
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.
Converts a natural number to USize, returning the largest representable value if the number is too
large.
Returns USize.size - 1, which is 2^64 - 1 or 2^32 - 1 depending on the platform, for natural
numbers greater than or equal to USize.size.
Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^8 - 1 for natural numbers greater than or equal to 2^8.
Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^16 - 1 for natural numbers greater than or equal to 2^16.
Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^32 - 1 for natural numbers greater than or equal to 2^32.
Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^64 - 1 for natural numbers greater than or equal to 2^64.
Converts a word-sized unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Converts a word-sized signed integer to a natural number, mapping all negative numbers to 0.
Use ISize.toBitVec to obtain the two's complement representation.
Converts an 8-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Converts an 8-bit signed integer to a natural number, mapping all negative numbers to 0.
Use Int8.toBitVec to obtain the two's complement representation.
Converts a 16-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Converts a 16-bit signed integer to a natural number, mapping all negative numbers to 0.
Use Int16.toBitVec to obtain the two's complement representation.
Converts a 32-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Converts a 32-bit signed integer to a natural number, mapping all negative numbers to 0.
Use Int32.toBitVec to obtain the two's complement representation.
Converts a 64-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Converts a 64-bit signed integer to a natural number, mapping all negative numbers to 0.
Use Int64.toBitVec to obtain the two's complement representation.
Converts word-sized unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts word-sized unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
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.
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.
Converts 8-bit unsigned integers to 16-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit unsigned integers to 32-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit unsigned integers to 64-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 16-bit unsigned integers to 32-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 16-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 32-bit unsigned integers to word-sized unsigned integers.
This function is overridden at runtime with an efficient implementation.
Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
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.
Converts a word-sized signed integer to an 8-bit signed integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts a word-sized integer to a 16-bit integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts a word-sized signed integer to a 32-bit signed integer.
On 32-bit platforms, this conversion is lossless. On 64-bit platforms, the integer's bitvector representation is truncated to 32 bits. This function is overridden at runtime with an efficient implementation.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit signed integers to 16-bit signed integers that denote the same number.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit signed integers to 32-bit signed integers that denote the same number.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit signed integers to 64-bit signed integers that denote the same number.
This function is overridden at runtime with an efficient implementation.
Converts 16-bit signed integers to 8-bit signed integers by truncating their bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts 8-bit signed integers to 32-bit signed integers that denote the same number.
This function is overridden at runtime with an efficient implementation.
Converts 16-bit signed integers to 64-bit signed integers that denote the same number.
This function is overridden at runtime with an efficient implementation.
Converts a 32-bit signed integer to an 8-bit signed integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts a 32-bit signed integer to an 16-bit signed integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts 32-bit signed integers to 64-bit signed integers that denote the same number.
This function is overridden at runtime with an efficient implementation.
Converts a 64-bit signed integer to an 8-bit signed integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts a 64-bit signed integer to a 16-bit signed integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts a 64-bit signed integer to a 32-bit signed integer by truncating its bitvector representation.
This function is overridden at runtime with an efficient implementation.
Converts 64-bit signed integers to word-sized signed integers, truncating the bitvector representation on 32-bit platforms. This conversion is lossless on 64-bit platforms.
This function is overridden at runtime with an efficient implementation.
Obtains a Float whose value is near the given ISize.
It will be exactly the value of the given ISize if such a Float exists. If no such Float
exists, the returned value will either be the smallest Float that is larger than the given value,
or the largest Float that is smaller than the given value.
This function has a logical model in terms of Float.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float32 whose value is near the given ISize.
It will be exactly the value of the given ISize if such a Float32 exists. If no such Float32
exists, the returned value will either be the smallest Float32 that is larger than the given
value, or the largest Float32 that is smaller than the given value.
This function has a logical model in terms of Float32.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float32 whose value is near the given Int32.
It will be exactly the value of the given Int32 if such a Float32 exists. If no such Float32
exists, the returned value will either be the smallest Float32 that is larger than the given
value, or the largest Float32 that is smaller than the given value.
This function has a logical model in terms of Float32.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float whose value is near the given Int64.
It will be exactly the value of the given Int64 if such a Float exists. If no such Float
exists, the returned value will either be the smallest Float that is larger than the given value,
or the largest Float that is smaller than the given value.
This function has a logical model in terms of Float.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float32 whose value is near the given Int64.
It will be exactly the value of the given Int64 if such a Float32 exists. If no such Float32
exists, the returned value will either be the smallest Float32 that is larger than the given
value, or the largest Float32 that is smaller than the given value.
This function has a logical model in terms of Float32.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float whose value is near the given USize.
It will be exactly the value of the given USize if such a Float exists. If no such Float
exists, the returned value will either be the smallest Float that is larger than the given value,
or the largest Float that is smaller than the given value.
This function has a logical model in terms of Float.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float32 whose value is near the given USize.
It will be exactly the value of the given USize if such a Float32 exists. If no such Float32
exists, the returned value will either be the smallest Float32 that is larger than the given
value, or the largest Float32 that is smaller than the given value.
This function has a logical model in terms of Float32.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float32 whose value is near the given UInt32.
It will be exactly the value of the given UInt32 if such a Float32 exists. If no such Float32
exists, the returned value will either be the smallest Float32 that is larger than the given
value, or the largest Float32 that is smaller than the given value.
This function has a logical model in terms of Float32.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float whose value is near the given UInt64.
It will be exactly the value of the given UInt64 if such a Float exists. If no such Float
exists, the returned value will either be the smallest Float that is larger than the given value,
or the largest Float that is smaller than the given value.
This function has a logical model in terms of Float.Model, but is overridden at runtime with an
efficient implementation.
Obtains a Float32 whose value is near the given UInt64.
It will be exactly the value of the given UInt64 if such a Float32 exists. If no such Float32
exists, the returned value will either be the smallest Float32 that is larger than the given
value, or the largest Float32 that is smaller than the given value.
This function has a logical model in terms of Float32.Model, but is overridden at runtime with an
efficient implementation.
Converts a word-sized unsigned integer into a decimal string.
This function is overridden at runtime with an efficient implementation.
Examples:
USize.repr 0 = "0"
USize.repr 28 = "28"
USize.repr 307 = "307"
The Char type is a wrapper around UInt32 that requires a proof that the wrapped integer represents a Unicode code point.
This predicate is part of the UInt32 API.
A UInt32 denotes a valid Unicode code point if it is less than 0x110000 and it is also not a
surrogate code point (the range 0xd800 to 0xdfff inclusive).
The operators in this section are rarely invoked by name.
Typically, comparisons operations on fixed-width integers should use the decidability of the corresponding relations, which consist of the equality type Eq and those implemented in instances of LE and LT.
Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
Non-strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the ≤ operator.
Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
Non-strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the ≤ operator.
Non-strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
Non-strict inequality of 16-bit signed integers, defined as inequality of the corresponding
integers. Usually accessed via the ≤ operator.
Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
Non-strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the ≤ operator.
Non-strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
Non-strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the ≤ operator.
Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
Strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the < operator.
Strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
Strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
Strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
Strict inequality of 16-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
Strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
Strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
Strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
Decides whether two word-sized unsigned integers are equal. Usually accessed via the
DecidableEq USize instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two word-sized signed integers are equal. Usually accessed via the
DecidableEq ISize instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 8-bit unsigned integers are equal. Usually accessed via the DecidableEq UInt8
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 8-bit signed integers are equal. Usually accessed via the DecidableEq Int8
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 16-bit unsigned integers are equal. Usually accessed via the
DecidableEq UInt16 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 16-bit signed integers are equal. Usually accessed via the DecidableEq Int16
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 32-bit unsigned integers are equal. Usually accessed via the
DecidableEq UInt32 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 32-bit signed integers are equal. Usually accessed via the DecidableEq Int32
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 64-bit unsigned integers are equal. Usually accessed via the
DecidableEq UInt64 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether two 64-bit signed integers are equal. Usually accessed via the DecidableEq Int64
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed
via the DecidableLE USize instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one word-sized signed integer is less than or equal to another. Usually accessed via
the DecidableLE ISize instance.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
Decides whether one 8-bit signed integer is less than or equal to another. Usually accessed via the
DecidableLE Int8 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
Decides whether one 16-bit signed integer is less than or equal to another. Usually accessed via the
DecidableLE Int16 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
DecidableLE UInt32 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
DecidableLE Int32 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
Decides whether one 8-bit signed integer is less than or equal to another. Usually accessed via the
DecidableLE Int64 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via
the DecidableLT USize instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one word-sized signed integer is strictly less than another. Usually accessed via the
DecidableLT ISize instance.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
Decides whether one 8-bit signed integer is strictly less than another. Usually accessed via the
DecidableLT Int8 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
Decides whether one 16-bit signed integer is strictly less than another. Usually accessed via the
DecidableLT Int16 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
DecidableLT UInt32 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Decides whether one 32-bit signed integer is strictly less than another. Usually accessed via the
DecidableLT Int32 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
Decides whether one 8-bit signed integer is strictly less than another. Usually accessed via the
DecidableLT Int64 instance.
This function is overridden at runtime with an efficient implementation.
Examples:
Typically, arithmetic operations on fixed-width integers should be accessed using Lean's overloaded arithmetic notation, particularly their instances of Add, Sub, Mul, Div, and Mod, as well as Neg for signed types.
Negates word-sized signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
Negates 8-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
Negates 16-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
Negates 32-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
Negates 64-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
Negation of word-sized unsigned integers, computed modulo USize.size.
This function is overridden at runtime with an efficient implementation.
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.
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.
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.
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.
Adds two word-sized unsigned integers, wrapping around on overflow. Usually accessed via the +
operator.
This function is overridden at runtime with an efficient implementation.
Adds two word-sized signed integers, wrapping around on over- or underflow. Usually accessed via
the + operator.
This function is overridden at runtime with an efficient implementation.
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.
Adds two 8-bit signed integers, wrapping around on over- or underflow. Usually accessed via the +
operator.
This function is overridden at runtime with an efficient implementation.
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.
Adds two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via the +
operator.
This function is overridden at runtime with an efficient implementation.
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.
Adds two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via the
+ operator.
This function is overridden at runtime with an efficient implementation.
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.
Adds two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via the
+ operator.
This function is overridden at runtime with an efficient implementation.
Subtracts one word-sized-bit unsigned integer from another, wrapping around on underflow. Usually
accessed via the - operator.
This function is overridden at runtime with an efficient implementation.
Subtracts one word-sized signed integer from another, wrapping around on over- or underflow. Usually
accessed via the - operator.
This function is overridden at runtime with an efficient implementation.
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.
Subtracts one 8-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the - operator.
This function is overridden at runtime with an efficient implementation.
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.
Subtracts one 16-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the - operator.
This function is overridden at runtime with an efficient implementation.
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.
Subtracts one 32-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the - operator.
This function is overridden at runtime with an efficient implementation.
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.
Subtracts one 64-bit signed integer from another, wrapping around on over- or underflow. Usually
accessed via the - operator.
This function is overridden at runtime with an efficient implementation.
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.
Multiplies two word-sized signed integers, wrapping around on over- or underflow. Usually accessed
via the * operator.
This function is overridden at runtime with an efficient implementation.
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.
Multiplies two 8-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the * operator.
This function is overridden at runtime with an efficient implementation.
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.
Multiplies two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the * operator.
This function is overridden at runtime with an efficient implementation.
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.
Multiplies two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the * operator.
This function is overridden at runtime with an efficient implementation.
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.
Multiplies two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via
the * operator.
This function is overridden at runtime with an efficient implementation.
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.
Truncating division for word-sized signed integers, rounding towards zero. Usually accessed via the
/ operator.
Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
Examples:
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.
Truncating division for 8-bit signed integers, rounding towards zero. Usually accessed via the /
operator.
Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
Examples:
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.
Truncating division for 16-bit signed integers, rounding towards zero. Usually accessed via the /
operator.
Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
Examples:
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.
Truncating division for 32-bit signed integers, rounding towards zero. Usually accessed via the /
operator.
Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
Examples:
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.
Truncating division for 64-bit signed integers, rounding towards zero. Usually accessed via the /
operator.
Division by zero is defined to be zero.
This function is overridden at runtime with an efficient implementation.
Examples:
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:
The modulo operator for word-sized signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by ISize.div. 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:
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:
The modulo operator for 8-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by Int8.div. 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:
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
The modulo operator for 16-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by Int16.div. 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:
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
The modulo operator for 32-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by Int32.div. 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:
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
The modulo operator for 64-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by Int64.div. 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:
Base-two logarithm of word-sized unsigned integers. Returns ⌊max 0 (log₂ a)⌋.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
USize.log2 0 = 0
USize.log2 1 = 0
USize.log2 2 = 1
USize.log2 4 = 2
USize.log2 7 = 2
USize.log2 8 = 3
Base-two logarithm of 8-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
UInt8.log2 0 = 0
UInt8.log2 1 = 0
UInt8.log2 2 = 1
UInt8.log2 4 = 2
UInt8.log2 7 = 2
UInt8.log2 8 = 3
Base-two logarithm of 16-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
UInt16.log2 0 = 0
UInt16.log2 1 = 0
UInt16.log2 2 = 1
UInt16.log2 4 = 2
UInt16.log2 7 = 2
UInt16.log2 8 = 3
Base-two logarithm of 32-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
UInt32.log2 0 = 0
UInt32.log2 1 = 0
UInt32.log2 2 = 1
UInt32.log2 4 = 2
UInt32.log2 7 = 2
UInt32.log2 8 = 3
Base-two logarithm of 64-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
UInt64.log2 0 = 0
UInt64.log2 1 = 0
UInt64.log2 2 = 1
UInt64.log2 4 = 2
UInt64.log2 7 = 2
UInt64.log2 8 = 3
Computes the absolute value of a word-sized signed integer.
This function is equivalent to if a < 0 then -a else a, so in particular ISize.minValue will be
mapped to ISize.minValue.
This function is overridden at runtime with an efficient implementation.
Computes the absolute value of an 8-bit signed integer.
This function is equivalent to if a < 0 then -a else a, so in particular Int8.minValue will be
mapped to Int8.minValue.
This function is overridden at runtime with an efficient implementation.
Computes the absolute value of a 16-bit signed integer.
This function is equivalent to if a < 0 then -a else a, so in particular Int16.minValue will be
mapped to Int16.minValue.
This function is overridden at runtime with an efficient implementation.
Computes the absolute value of a 32-bit signed integer.
This function is equivalent to if a < 0 then -a else a, so in particular Int32.minValue will be
mapped to Int32.minValue.
This function is overridden at runtime with an efficient implementation.
Computes the absolute value of a 64-bit signed integer.
This function is equivalent to if a < 0 then -a else a, so in particular Int64.minValue will be
mapped to Int64.minValue.
This function is overridden at runtime with an efficient implementation.
Typically, bitwise operations on fixed-width integers should be accessed using Lean's overloaded operators, particularly their instances of ShiftLeft, ShiftRight, AndOp, OrOp, and XorOp.
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.
Bitwise and for word-sized signed integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise and for 8-bit signed integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise and for 16-bit signed integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise and for 32-bit signed integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise and for 64-bit signed integers. Usually accessed via the &&& operator.
Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise or for word-sized signed integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise or for 8-bit signed integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise or for 16-bit signed integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise or for 32-bit signed integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise or for 64-bit signed integers. Usually accessed via the ||| operator.
Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise exclusive or for word-sized signed integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise exclusive or for 8-bit signed integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise exclusive or for 16-bit signed integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise exclusive or for 32-bit signed integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise exclusive or for 64-bit signed integers. Usually accessed via the ^^^ operator.
Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
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.
Bitwise complement, also known as bitwise negation, for word-sized signed integers. Usually accessed
via the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so ISize.complement a = -(a + 1).
This function is overridden at runtime with an efficient implementation.
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.
Bitwise complement, also known as bitwise negation, for 8-bit signed integers. Usually accessed via
the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so Int8.complement a = -(a + 1).
This function is overridden at runtime with an efficient implementation.
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.
Bitwise complement, also known as bitwise negation, for 16-bit signed integers. Usually accessed via
the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so Int16.complement a = -(a + 1).
This function is overridden at runtime with an efficient implementation.
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.
Bitwise complement, also known as bitwise negation, for 32-bit signed integers. Usually accessed via
the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so Int32.complement a = -(a + 1).
This function is overridden at runtime with an efficient implementation.
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.
Bitwise complement, also known as bitwise negation, for 64-bit signed integers. Usually accessed via
the ~~~ prefix operator.
Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so Int64.complement a = -(a + 1).
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for word-sized unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for word-sized signed integers. Usually accessed via the <<< operator.
Signed integers are interpreted as bitvectors according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 8-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 8-bit signed integers. Usually accessed via the <<< operator.
Signed integers are interpreted as bitvectors according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 16-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 16-bit signed integers. Usually accessed via the <<< operator.
Signed integers are interpreted as bitvectors according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 32-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 32-bit signed integers. Usually accessed via the <<< operator.
Signed integers are interpreted as bitvectors according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 64-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
Bitwise left shift for 64-bit signed integers. Usually accessed via the <<< operator.
Signed integers are interpreted as bitvectors according to the two's complement representation.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for word-sized unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Arithmetic right shift for word-sized signed integers. Usually accessed via the <<< operator.
The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 8-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Arithmetic right shift for 8-bit signed integers. Usually accessed via the <<< operator.
The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 16-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Arithmetic right shift for 16-bit signed integers. Usually accessed via the <<< operator.
The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 32-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Arithmetic right shift for 32-bit signed integers. Usually accessed via the <<< operator.
The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.
Bitwise right shift for 64-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
Arithmetic right shift for 64-bit signed integers. Usually accessed via the <<< operator.
The high bits are filled with the value of the most significant bit.
This function is overridden at runtime with an efficient implementation.