20.4.4.4. Comparisons🔗
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.
🔗def
Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 16-bit signed integers, defined as inequality of the corresponding
integers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the ≤ operator.
🔗def
Non-strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the ≤ operator.
🔗def
Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
🔗def
Strict inequality of word-sized signed integers, defined as inequality of the corresponding
integers. Usually accessed via the < operator.
🔗def
Strict inequality of 8-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
🔗def
Strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
🔗def
Strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
🔗def
Strict inequality of 16-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
🔗def
Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
🔗def
Strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
🔗def
Strict inequality of 64-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the < operator.
🔗def
Strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the < operator.
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
20.4.4.5. Arithmetic🔗
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.
🔗def
Negates word-sized signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
🔗def
Negates 8-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
🔗def
Negates 16-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
🔗def
Negates 32-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
🔗def
Negates 64-bit signed integers. Usually accessed via the - prefix operator.
This function is overridden at runtime with an efficient implementation.
🔗def
Negation of word-sized unsigned integers, computed modulo USize.size.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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:
🔗def
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.
🔗def
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:
🔗def
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.
🔗def
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:
🔗def
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.
🔗def
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:
🔗def
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.
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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:
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
20.4.4.6. Bitwise Operations🔗
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
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.
🔗def
Bitwise left shift for word-sized unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise left shift for 8-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise left shift for 16-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise left shift for 32-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise left shift for 64-bit unsigned integers. Usually accessed via the <<< operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise right shift for word-sized unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise right shift for 8-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise right shift for 16-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise right shift for 32-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
🔗def
Bitwise right shift for 64-bit unsigned integers. Usually accessed via the >>> operator.
This function is overridden at runtime with an efficient implementation.
🔗def
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.
