18.4. Fixed-Precision Integers🔗

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.

18.4.1. Logical Model

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.

18.4.1.1. Unsigned

structure

USize : Type

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.

structure

UInt8 : Type

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

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

Fields

toBitVec : BitVec 8

Unpacks a UInt8 into a BitVec 8. This function is overridden with a native implementation.

structure

UInt16 : Type

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

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

Fields

toBitVec : BitVec 16

Unpacks a UInt16 into a BitVec 16. This function is overridden with a native implementation.

structure

UInt32 : Type

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

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

Fields

toBitVec : BitVec 32

Unpacks a UInt32 into a BitVec 32. This function is overridden with a native implementation.

structure

UInt64 : Type

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

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

Fields

toBitVec : BitVec 64

Unpacks a UInt64 into a BitVec 64. This function is overridden with a native implementation.

18.4.1.2. Signed

structure

ISize : Type

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.

Fields

toUSize : USize

Converts a word-sized signed integer into the word-sized unsigned integer that is its two's complement encoding.

structure

Int8 : Type

Signed 8-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 8-bit value.

Fields

toUInt8 : UInt8

Converts an 8-bit signed integer into the 8-bit unsigned integer that is its two's complement encoding.

structure

Int16 : Type

Signed 16-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 16-bit value.

Fields

toUInt16 : UInt16

Converts an 16-bit signed integer into the 16-bit unsigned integer that is its two's complement encoding.

structure

Int32 : Type

Signed 32-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 32-bit value.

Fields

toUInt32 : UInt32

Converts an 32-bit signed integer into the 32-bit unsigned integer that is its two's complement encoding.

structure

Int64 : Type

Signed 64-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 64-bit value.

Fields

toUInt64 : UInt64

Converts an 64-bit signed integer into the 64-bit unsigned integer that is its two's complement encoding.

18.4.2. Run-Time Representation

In compiled code, fixed-width integer types that fit in one less bit than the platform's pointer size are always represented unboxed, without additional allocations or indirections. This always includes Int8, UInt8, Int16, and UInt16. On 64-bit architectures, Int32 and UInt32 are also unboxed. On 32-bit architectures, Int32 and UInt32 are boxed, which means they may be represented by a pointer to an object on the heap. ISize, USize, Int64 and UInt64 are boxed on all architectures.

Even though some fixed-with integer types require boxing in general, the compiler is able to represent them without boxing 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.The 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.

18.4.3. Syntax

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.

Fixed-Width Literals

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.

Overflowing Fixed-Width Literals

The following statements are all true:

example : (255 : UInt8) = 255 := by⊢ 255 = 255 rflAll goals completed! 🐙
example : (256 : UInt8) = 0   := by⊢ 256 = 0 rflAll goals completed! 🐙
example : (257 : UInt8) = 1   := by⊢ 257 = 1 rflAll goals completed! 🐙

example : (0x7f : Int8) = 127  := by⊢ 127 = 127 rflAll goals completed! 🐙
example : (0x8f : Int8) = -113 := by⊢ 143 = -113 rflAll goals completed! 🐙
example : (0xff : Int8) = -1   := by⊢ 255 = -1 rflAll goals completed! 🐙

18.4.4. API Reference

18.4.4.1. Sizes

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.

def

USize.size : Nat

The number of distinct values representable by USize, that is, 2^System.Platform.numBits.

def

ISize.size : Nat

The number of distinct values representable by ISize, that is, 2^System.Platform.numBits.

def

UInt8.size : Nat

The number of distinct values representable by UInt8, that is, 2^8 = 256.

def

Int8.size : Nat

The number of distinct values representable by Int8, that is, 2^8 = 256.

def

UInt16.size : Nat

The number of distinct values representable by UInt16, that is, 2^16 = 65536.

def

Int16.size : Nat

The number of distinct values representable by Int16, that is, 2^16 = 65536.

def

UInt32.size : Nat

The number of distinct values representable by UInt32, that is, 2^32 = 4294967296.

def

Int32.size : Nat

The number of distinct values representable by Int32, that is, 2^32 = 4294967296.

def

UInt64.size : Nat

The number of distinct values representable by UInt64, that is, 2^64 = 18446744073709551616.

def

Int64.size : Nat

The number of distinct values representable by Int64, that is, 2^64 = 18446744073709551616.

18.4.4.2. Ranges

def

ISize.minValue : ISize

The smallest number that ISize can represent: -2^(System.Platform.numBits - 1).

def

ISize.maxValue : ISize

The largest number that ISize can represent: 2^(System.Platform.numBits - 1) - 1.

def

Int8.minValue : Int8

The smallest number that Int8 can represent: -2^7 = -128.

def

Int8.maxValue : Int8

The largest number that Int8 can represent: 2^7 - 1 = 127.

def

Int16.minValue : Int16

The smallest number that Int16 can represent: -2^15 = -32768.

def

Int16.maxValue : Int16

The largest number that Int16 can represent: 2^15 - 1 = 32767.

def

Int32.minValue : Int32

The smallest number that Int32 can represent: -2^31 = -2147483648.

def

Int32.maxValue : Int32

The largest number that Int32 can represent: 2^31 - 1 = 2147483647.

def

Int64.minValue : Int64

The smallest number that Int64 can represent: -2^63 = -9223372036854775808.

def

Int64.maxValue : Int64

The largest number that Int64 can represent: 2^63 - 1 = 9223372036854775807.

18.4.4.3. Conversions

18.4.4.3.1. To and From `Int`

def

ISize.toInt (i : ISize) : Int

Converts 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.

def

Int8.toInt (i : Int8) : Int

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.

def

Int16.toInt (i : Int16) : Int

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.

def

Int32.toInt (i : Int32) : Int

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.

def

Int64.toInt (i : Int64) : Int

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.

def

ISize.ofInt (i : Int) : ISize

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.

def

Int8.ofInt (i : Int) : Int8

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

def

Int16.ofInt (i : Int) : Int16

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

def

Int32.ofInt (i : Int) : Int32

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

def

Int64.ofInt (i : Int) : Int64

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

def

ISize.ofIntTruncate (i : Int) : ISize

Constructs an ISize from an Int, clamping if the value is too small or too large.

def

Int8.ofIntTruncate (i : Int) : Int8

Constructs an Int8 from an Int, clamping if the value is too small or too large.

def

Int16.ofIntTruncate (i : Int) : Int16

Constructs an Int16 from an Int, clamping if the value is too small or too large.

def

Int32.ofIntTruncate (i : Int) : Int32

Constructs an Int32 from an Int, clamping if the value is too small or too large.

def

Int64.ofIntTruncate (i : Int) : Int64

Constructs an Int64 from an Int, clamping if the value is too small or too large.

def

ISize.ofIntLE (i : Int)
  (_hl : ISize.minValue.toInt ≤ i)
  (_hr : i ≤ ISize.maxValue.toInt) : ISize

Constructs an ISize from an Int that is known to be in bounds.

def

Int8.ofIntLE (i : Int)
  (_hl : Int8.minValue.toInt ≤ i)
  (_hr : i ≤ Int8.maxValue.toInt) : Int8

Constructs an Int8 from an Int that is known to be in bounds.

def

Int16.ofIntLE (i : Int)
  (_hl : Int16.minValue.toInt ≤ i)
  (_hr : i ≤ Int16.maxValue.toInt) : Int16

Constructs an Int16 from an Int that is known to be in bounds.

def

Int32.ofIntLE (i : Int)
  (_hl : Int32.minValue.toInt ≤ i)
  (_hr : i ≤ Int32.maxValue.toInt) : Int32

Constructs an Int32 from an Int that is known to be in bounds.

def

Int64.ofIntLE (i : Int)
  (_hl : Int64.minValue.toInt ≤ i)
  (_hr : i ≤ Int64.maxValue.toInt) : Int64

Constructs an Int64 from an Int that is known to be in bounds.

18.4.4.3.2. To and From `Nat`

def

USize.ofNat (n : Nat) : USize

Converts 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.

def

ISize.ofNat (n : Nat) : ISize

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.

def

UInt8.ofNat (n : Nat) : UInt8

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

def

Int8.ofNat (n : Nat) : Int8

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

def

UInt16.ofNat (n : Nat) : UInt16

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

def

Int16.ofNat (n : Nat) : Int16

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

def

UInt32.ofNat (n : Nat) : UInt32

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

def

Int32.ofNat (n : Nat) : Int32

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

def

UInt64.ofNat (n : Nat) : UInt64

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

def

Int64.ofNat (n : Nat) : Int64

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

def

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

Converts a natural number to a USize. Overflow is impossible on any supported platform because USize.size is either 2^32 or 2^64.

This function is overridden at runtime with an efficient implementation.

def

USize.ofNatLT (n : Nat) (h : n < USize.size) :
  USize

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

This function is overridden at runtime with an efficient implementation.

def

UInt8.ofNatLT (n : Nat) (h : n < UInt8.size) :
  UInt8

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

This function is overridden at runtime with an efficient implementation.

def

UInt16.ofNatLT (n : Nat) (h : n < UInt16.size) :
  UInt16

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

This function is overridden at runtime with an efficient implementation.

def

UInt32.ofNatLT (n : Nat) (h : n < UInt32.size) :
  UInt32

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

This function is overridden at runtime with an efficient implementation.

def

UInt64.ofNatLT (n : Nat) (h : n < UInt64.size) :
  UInt64

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

This function is overridden at runtime with an efficient implementation.

def

USize.ofNatTruncate (n : Nat) : USize

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.

def

UInt8.ofNatTruncate (n : Nat) : UInt8

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.

def

UInt16.ofNatTruncate (n : Nat) : UInt16

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.

def

UInt32.ofNatTruncate (n : Nat) : UInt32

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.

def

UInt64.ofNatTruncate (n : Nat) : UInt64

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.

def

USize.toNat (n : USize) : Nat

Converts a word-sized unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

def

ISize.toNatClampNeg (i : ISize) : Nat

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.

def

UInt8.toNat (n : UInt8) : Nat

Converts an 8-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

def

Int8.toNatClampNeg (i : Int8) : Nat

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.

def

UInt16.toNat (n : UInt16) : Nat

Converts a 16-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

def

Int16.toNatClampNeg (i : Int16) : Nat

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.

def

UInt32.toNat (n : UInt32) : Nat

Converts a 32-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

def

Int32.toNatClampNeg (i : Int32) : Nat

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.

def

UInt64.toNat (n : UInt64) : Nat

Converts a 64-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

def

Int64.toNatClampNeg (i : Int64) : Nat

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.

18.4.4.3.3. To Other Fixed-Width Integers

def

USize.toUInt8 (a : USize) : UInt8

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

This function is overridden at runtime with an efficient implementation.

def

USize.toUInt16 (a : USize) : UInt16

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

This function is overridden at runtime with an efficient implementation.

def

USize.toUInt32 (a : USize) : UInt32

Converts word-sized unsigned integers to 32-bit unsigned integers. Wraps around on overflow, which might occur on 64-bit architectures.

This function is overridden at runtime with an efficient implementation.

def

USize.toUInt64 (a : USize) : UInt64

Converts word-sized unsigned integers to 32-bit unsigned integers. This cannot overflow because USize.size is either 2^32 or 2^64.

This function is overridden at runtime with an efficient implementation.

def

USize.toISize (i : USize) : ISize

Obtains the ISize that is 2's complement equivalent to the USize.

def

UInt8.toInt8 (i : UInt8) : Int8

Obtains the Int8 that is 2's complement equivalent to the UInt8.

def

UInt8.toUInt16 (a : UInt8) : UInt16

Converts 8-bit unsigned integers to 16-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

def

UInt8.toUInt32 (a : UInt8) : UInt32

Converts 8-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

def

UInt8.toUInt64 (a : UInt8) : UInt64

Converts 8-bit unsigned integers to 64-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

def

UInt8.toUSize (a : UInt8) : USize

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

This function is overridden at runtime with an efficient implementation.

def

UInt16.toUInt8 (a : UInt16) : UInt8

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

This function is overridden at runtime with an efficient implementation.

def

UInt16.toInt16 (i : UInt16) : Int16

Obtains the Int16 that is 2's complement equivalent to the UInt16.

def

UInt16.toUInt32 (a : UInt16) : UInt32

Converts 16-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

def

UInt16.toUInt64 (a : UInt16) : UInt64

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

This function is overridden at runtime with an efficient implementation.

def

UInt16.toUSize (a : UInt16) : USize

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

This function is overridden at runtime with an efficient implementation.

def

UInt32.toUInt8 (a : UInt32) : UInt8

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.

def

UInt32.toUInt16 (a : UInt32) : UInt16

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

This function is overridden at runtime with an efficient implementation.

def

UInt32.toInt32 (i : UInt32) : Int32

Obtains the Int32 that is 2's complement equivalent to the UInt32.

def

UInt32.toUInt64 (a : UInt32) : UInt64

Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

def

UInt32.toUSize (a : UInt32) : USize

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

This function is overridden at runtime with an efficient implementation.

def

UInt64.toUInt8 (a : UInt64) : UInt8

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

This function is overridden at runtime with an efficient implementation.

def

UInt64.toUInt16 (a : UInt64) : UInt16

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

This function is overridden at runtime with an efficient implementation.

def

UInt64.toUInt32 (a : UInt64) : UInt32

Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

def

UInt64.toInt64 (i : UInt64) : Int64

Obtains the Int64 that is 2's complement equivalent to the UInt64.

def

UInt64.toUSize (a : UInt64) : USize

Converts 64-bit unsigned integers to word-sized unsigned integers. On 32-bit machines, this may overflow, which results in the value wrapping around (that is, it is reduced modulo USize.size).

This function is overridden at runtime with an efficient implementation.

def

ISize.toInt8 (a : ISize) : Int8

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.

def

ISize.toInt16 (a : ISize) : Int16

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.

def

ISize.toInt32 (a : ISize) : Int32

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.

def

ISize.toInt64 (a : ISize) : Int64

Converts word-sized signed integers to 64-bit signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

def

Int8.toInt16 (a : Int8) : Int16

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.

def

Int8.toInt32 (a : Int8) : Int32

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.

def

Int8.toInt64 (a : Int8) : Int64

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.

def

Int8.toISize (a : Int8) : ISize

Converts 8-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

def

Int16.toInt8 (a : Int16) : Int8

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.

def

Int16.toInt32 (a : Int16) : Int32

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.

def

Int16.toInt64 (a : Int16) : Int64

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.

def

Int16.toISize (a : Int16) : ISize

Converts 16-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

def

Int32.toInt8 (a : Int32) : Int8

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.

def

Int32.toInt16 (a : Int32) : Int16

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.

def

Int32.toInt64 (a : Int32) : Int64

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.

def

Int32.toISize (a : Int32) : ISize

Converts 32-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

def

Int64.toInt8 (a : Int64) : Int8

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.

def

Int64.toInt16 (a : Int64) : Int16

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.

def

Int64.toInt32 (a : Int64) : Int32

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.

def

Int64.toISize (a : Int64) : ISize

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.

18.4.4.3.4. To Floating-Point Numbers

opaque

ISize.toFloat (n : ISize) : Float

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 does not reduce in the kernel.

opaque

ISize.toFloat32 (n : ISize) : Float32

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 does not reduce in the kernel.

opaque

Int8.toFloat (n : Int8) : Float

Obtains the Float whose value is the same as the given Int8.

This function does not reduce in the kernel.

opaque

Int8.toFloat32 (n : Int8) : Float32

Obtains the Float32 whose value is the same as the given Int8.

This function does not reduce in the kernel.

opaque

Int16.toFloat (n : Int16) : Float

Obtains the Float whose value is the same as the given Int16.

This function does not reduce in the kernel.

opaque

Int16.toFloat32 (n : Int16) : Float32

Obtains the Float32 whose value is the same as the given Int16.

This function does not reduce in the kernel.

opaque

Int32.toFloat (n : Int32) : Float

Obtains the Float whose value is the same as the given Int32.

This function does not reduce in the kernel.

opaque

Int32.toFloat32 (n : Int32) : Float32

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 does not reduce in the kernel.

opaque

Int64.toFloat (n : Int64) : Float

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 does not reduce in the kernel.

opaque

Int64.toFloat32 (n : Int64) : Float32

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 does not reduce in the kernel.

opaque

USize.toFloat (n : USize) : Float

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 is opaque in the kernel, but is overridden at runtime with an efficient implementation.

opaque

USize.toFloat32 (n : USize) : Float32

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 is opaque in the kernel, but is overridden at runtime with an efficient implementation.

opaque

UInt8.toFloat (n : UInt8) : Float

Obtains the Float whose value is the same as the given UInt8.

opaque

UInt8.toFloat32 (n : UInt8) : Float32

Obtains the Float32 whose value is the same as the given UInt8.

opaque

UInt16.toFloat (n : UInt16) : Float

Obtains the Float whose value is the same as the given UInt16.

opaque

UInt16.toFloat32 (n : UInt16) : Float32

Obtains the Float32 whose value is the same as the given UInt16.

opaque

UInt32.toFloat (n : UInt32) : Float

Obtains the Float whose value is the same as the given UInt32.

opaque

UInt32.toFloat32 (n : UInt32) : Float32

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 is opaque in the kernel, but is overridden at runtime with an efficient implementation.

opaque

UInt64.toFloat (n : UInt64) : Float

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 is opaque in the kernel, but is overridden at runtime with an efficient implementation.

opaque

UInt64.toFloat32 (n : UInt64) : Float32

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 is opaque in the kernel, but is overridden at runtime with an efficient implementation.

18.4.4.3.5. To and From Bitvectors

def

ISize.toBitVec (x : ISize) :
  BitVec System.Platform.numBits

Obtain the BitVec that contains the 2's complement representation of the ISize.

def

ISize.ofBitVec
  (b : BitVec System.Platform.numBits) : ISize

Obtains the ISize whose 2's complement representation is the given BitVec.

def

Int8.toBitVec (x : Int8) : BitVec 8

Obtain the BitVec that contains the 2's complement representation of the Int8.

def

Int8.ofBitVec (b : BitVec 8) : Int8

Obtains the Int8 whose 2's complement representation is the given BitVec 8.

def

Int16.toBitVec (x : Int16) : BitVec 16

Obtain the BitVec that contains the 2's complement representation of the Int16.

def

Int16.ofBitVec (b : BitVec 16) : Int16

Obtains the Int16 whose 2's complement representation is the given BitVec 16.

def

Int32.toBitVec (x : Int32) : BitVec 32

Obtain the BitVec that contains the 2's complement representation of the Int32.

def

Int32.ofBitVec (b : BitVec 32) : Int32

Obtains the Int32 whose 2's complement representation is the given BitVec 32.

def

Int64.toBitVec (x : Int64) : BitVec 64

Obtain the BitVec that contains the 2's complement representation of the Int64.

def

Int64.ofBitVec (b : BitVec 64) : Int64

Obtains the Int64 whose 2's complement representation is the given BitVec 64.

18.4.4.3.6. To and From Finite Numbers

def

USize.toFin (x : USize) : Fin USize.size

Converts a USize into the corresponding Fin USize.size.

def

UInt8.toFin (x : UInt8) : Fin UInt8.size

Converts a UInt8 into the corresponding Fin UInt8.size.

def

UInt16.toFin (x : UInt16) : Fin UInt16.size

Converts a UInt16 into the corresponding Fin UInt16.size.

def

UInt32.toFin (x : UInt32) : Fin UInt32.size

Converts a UInt32 into the corresponding Fin UInt32.size.

def

UInt64.toFin (x : UInt64) : Fin UInt64.size

Converts a UInt64 into the corresponding Fin UInt64.size.

def

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

Converts a Fin USize.size into the corresponding USize.

def

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

Converts a Fin UInt8.size into the corresponding UInt8.

def

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

Converts a Fin UInt16.size into the corresponding UInt16.

def

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

Converts a Fin UInt32.size into the corresponding UInt32.

def

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

Converts a Fin UInt64.size into the corresponding UInt64.

def

USize.repr (n : USize) : String

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"

18.4.4.3.7. To Characters

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.

def

UInt32.isValidChar (n : UInt32) : Prop

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

18.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

USize.le (a b : USize) : Prop

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

def

ISize.le (a b : ISize) : Prop

Non-strict inequality of word-sized signed integers, defined as inequality of the corresponding integers. Usually accessed via the ≤ operator.

def

UInt8.le (a b : UInt8) : Prop

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

def

Int8.le (a b : Int8) : Prop

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

def

UInt16.le (a b : UInt16) : Prop

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

def

Int16.le (a b : Int16) : Prop

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

def

UInt32.le (a b : UInt32) : Prop

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

def

Int32.le (a b : Int32) : Prop

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

def

UInt64.le (a b : UInt64) : Prop

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

def

Int64.le (a b : Int64) : Prop

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

def

USize.lt (a b : USize) : Prop

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

def

ISize.lt (a b : ISize) : Prop

Strict inequality of word-sized signed integers, defined as inequality of the corresponding integers. Usually accessed via the < operator.

def

UInt8.lt (a b : UInt8) : Prop

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

def

Int8.lt (a b : Int8) : Prop

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

def

UInt16.lt (a b : UInt16) : Prop

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

def

Int16.lt (a b : Int16) : Prop

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

def

UInt32.lt (a b : UInt32) : Prop

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

def

Int32.lt (a b : Int32) : Prop

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

def

UInt64.lt (a b : UInt64) : Prop

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

def

Int64.lt (a b : Int64) : Prop

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

def

USize.decEq (a b : USize) : Decidable (a = b)

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:

USize.decEq 123 123 = .isTrue rfl
(if (6 : USize) = 7 then "yes" else "no") = "no"
show (7 : USize) = 7 by decide

def

ISize.decEq (a b : ISize) : Decidable (a = b)

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:

ISize.decEq 123 123 = .isTrue rfl
(if ((-7) : ISize) = 7 then "yes" else "no") = "no"
show (7 : ISize) = 7 by decide

def

UInt8.decEq (a b : UInt8) : Decidable (a = b)

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:

UInt8.decEq 123 123 = .isTrue rfl
(if (6 : UInt8) = 7 then "yes" else "no") = "no"
show (7 : UInt8) = 7 by decide

def

Int8.decEq (a b : Int8) : Decidable (a = b)

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:

Int8.decEq 123 123 = .isTrue rfl
(if ((-7) : Int8) = 7 then "yes" else "no") = "no"
show (7 : Int8) = 7 by decide

def

UInt16.decEq (a b : UInt16) : Decidable (a = b)

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:

UInt16.decEq 123 123 = .isTrue rfl
(if (6 : UInt16) = 7 then "yes" else "no") = "no"
show (7 : UInt16) = 7 by decide

def

Int16.decEq (a b : Int16) : Decidable (a = b)

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:

Int16.decEq 123 123 = .isTrue rfl
(if ((-7) : Int16) = 7 then "yes" else "no") = "no"
show (7 : Int16) = 7 by decide

def

UInt32.decEq (a b : UInt32) : Decidable (a = b)

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:

UInt32.decEq 123 123 = .isTrue rfl
(if (6 : UInt32) = 7 then "yes" else "no") = "no"
show (7 : UInt32) = 7 by decide

def

Int32.decEq (a b : Int32) : Decidable (a = b)

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:

Int32.decEq 123 123 = .isTrue rfl
(if ((-7) : Int32) = 7 then "yes" else "no") = "no"
show (7 : Int32) = 7 by decide

def

UInt64.decEq (a b : UInt64) : Decidable (a = b)

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:

UInt64.decEq 123 123 = .isTrue rfl
(if (6 : UInt64) = 7 then "yes" else "no") = "no"
show (7 : UInt64) = 7 by decide

def

Int64.decEq (a b : Int64) : Decidable (a = b)

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:

Int64.decEq 123 123 = .isTrue rfl
(if ((-7) : Int64) = 7 then "yes" else "no") = "no"
show (7 : Int64) = 7 by decide

def

USize.decLe (a b : USize) : Decidable (a ≤ b)

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:

(if (15 : USize) ≤ 15 then "yes" else "no") = "yes"
(if (15 : USize) ≤ 5 then "yes" else "no") = "no"
(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"
show (7 : USize) ≤ 7 by decide

def

ISize.decLe (a b : ISize) : Decidable (a ≤ b)

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:

(if ((-7) : ISize) ≤ 7 then "yes" else "no") = "yes"
(if (15 : ISize) ≤ 15 then "yes" else "no") = "yes"
(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"
show (7 : ISize) ≤ 7 by decide

def

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

Decides whether one 8-bit unsigned integer is less than or equal to another. Usually accessed via the DecidableLE UInt8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

(if (15 : UInt8) ≤ 15 then "yes" else "no") = "yes"
(if (15 : UInt8) ≤ 5 then "yes" else "no") = "no"
(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"
show (7 : UInt8) ≤ 7 by decide

def

Int8.decLe (a b : Int8) : Decidable (a ≤ b)

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:

(if ((-7) : Int8) ≤ 7 then "yes" else "no") = "yes"
(if (15 : Int8) ≤ 15 then "yes" else "no") = "yes"
(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"
show (7 : Int8) ≤ 7 by decide

def

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

Decides whether one 16-bit unsigned integer is less than or equal to another. Usually accessed via the DecidableLE UInt16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

(if (15 : UInt16) ≤ 15 then "yes" else "no") = "yes"
(if (15 : UInt16) ≤ 5 then "yes" else "no") = "no"
(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"
show (7 : UInt16) ≤ 7 by decide

def

Int16.decLe (a b : Int16) : Decidable (a ≤ b)

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:

(if ((-7) : Int16) ≤ 7 then "yes" else "no") = "yes"
(if (15 : Int16) ≤ 15 then "yes" else "no") = "yes"
(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"
show (7 : Int16) ≤ 7 by decide

def

UInt32.decLe (a b : UInt32) : Decidable (a ≤ b)

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:

(if (15 : UInt32) ≤ 15 then "yes" else "no") = "yes"
(if (15 : UInt32) ≤ 5 then "yes" else "no") = "no"
(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"
show (7 : UInt32) ≤ 7 by decide

def

Int32.decLe (a b : Int32) : Decidable (a ≤ b)

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:

(if ((-7) : Int32) ≤ 7 then "yes" else "no") = "yes"
(if (15 : Int32) ≤ 15 then "yes" else "no") = "yes"
(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"
show (7 : Int32) ≤ 7 by decide

def

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

Decides whether one 64-bit unsigned integer is less than or equal to another. Usually accessed via the DecidableLE UInt64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

(if (15 : UInt64) ≤ 15 then "yes" else "no") = "yes"
(if (15 : UInt64) ≤ 5 then "yes" else "no") = "no"
(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"
show (7 : UInt64) ≤ 7 by decide

def

Int64.decLe (a b : Int64) : Decidable (a ≤ b)

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:

(if ((-7) : Int64) ≤ 7 then "yes" else "no") = "yes"
(if (15 : Int64) ≤ 15 then "yes" else "no") = "yes"
(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"
show (7 : Int64) ≤ 7 by decide

def

USize.decLt (a b : USize) : Decidable (a < b)

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:

(if (6 : USize) < 7 then "yes" else "no") = "yes"
(if (5 : USize) < 5 then "yes" else "no") = "no"
show ¬((7 : USize) < 7) by decide

def

ISize.decLt (a b : ISize) : Decidable (a < b)

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:

(if ((-7) : ISize) < 7 then "yes" else "no") = "yes"
(if (5 : ISize) < 5 then "yes" else "no") = "no"
show ¬((7 : ISize) < 7) by decide

def

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

Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the DecidableLT UInt8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

(if (6 : UInt8) < 7 then "yes" else "no") = "yes"
(if (5 : UInt8) < 5 then "yes" else "no") = "no"
show ¬((7 : UInt8) < 7) by decide

def

Int8.decLt (a b : Int8) : Decidable (a < b)

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:

(if ((-7) : Int8) < 7 then "yes" else "no") = "yes"
(if (5 : Int8) < 5 then "yes" else "no") = "no"
show ¬((7 : Int8) < 7) by decide

def

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

Decides whether one 16-bit unsigned integer is strictly less than another. Usually accessed via the DecidableLT UInt16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

(if (6 : UInt16) < 7 then "yes" else "no") = "yes"
(if (5 : UInt16) < 5 then "yes" else "no") = "no"
show ¬((7 : UInt16) < 7) by decide

def

Int16.decLt (a b : Int16) : Decidable (a < b)

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:

(if ((-7) : Int16) < 7 then "yes" else "no") = "yes"
(if (5 : Int16) < 5 then "yes" else "no") = "no"
show ¬((7 : Int16) < 7) by decide

def

UInt32.decLt (a b : UInt32) : Decidable (a < b)

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:

(if (6 : UInt32) < 7 then "yes" else "no") = "yes"
(if (5 : UInt32) < 5 then "yes" else "no") = "no"
show ¬((7 : UInt32) < 7) by decide

def

Int32.decLt (a b : Int32) : Decidable (a < b)

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:

(if ((-7) : Int32) < 7 then "yes" else "no") = "yes"
(if (5 : Int32) < 5 then "yes" else "no") = "no"
show ¬((7 : Int32) < 7) by decide

def

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

Decides whether one 64-bit unsigned integer is strictly less than another. Usually accessed via the DecidableLT UInt64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

(if (6 : UInt64) < 7 then "yes" else "no") = "yes"
(if (5 : UInt64) < 5 then "yes" else "no") = "no"
show ¬((7 : UInt64) < 7) by decide

def

Int64.decLt (a b : Int64) : Decidable (a < b)

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:

(if ((-7) : Int64) < 7 then "yes" else "no") = "yes"
(if (5 : Int64) < 5 then "yes" else "no") = "no"
show ¬((7 : Int64) < 7) by decide

18.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

ISize.neg (i : ISize) : ISize

Negates word-sized signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

def

Int8.neg (i : Int8) : Int8

Negates 8-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

def

Int16.neg (i : Int16) : Int16

Negates 16-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

def

Int32.neg (i : Int32) : Int32

Negates 32-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

def

Int64.neg (i : Int64) : Int64

Negates 64-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

def

USize.neg (a : USize) : USize

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

This function is overridden at runtime with an efficient implementation.

def

UInt8.neg (a : UInt8) : UInt8

Negation of 8-bit unsigned integers, computed modulo UInt8.size.

UInt8.neg a is equivalent to 255 - a + 1.

This function is overridden at runtime with an efficient implementation.

def

UInt16.neg (a : UInt16) : UInt16

Negation of 16-bit unsigned integers, computed modulo UInt16.size.

UInt16.neg a is equivalent to 65_535 - a + 1.

This function is overridden at runtime with an efficient implementation.

def

UInt32.neg (a : UInt32) : UInt32

Negation of 32-bit unsigned integers, computed modulo UInt32.size.

UInt32.neg a is equivalent to 429_4967_295 - a + 1.

This function is overridden at runtime with an efficient implementation.

def

UInt64.neg (a : UInt64) : UInt64

Negation of 32-bit unsigned integers, computed modulo UInt64.size.

UInt64.neg a is equivalent to 18_446_744_073_709_551_615 - a + 1.

This function is overridden at runtime with an efficient implementation.

def

USize.add (a b : USize) : USize

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

ISize.add (a b : ISize) : ISize

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

UInt8.add (a b : UInt8) : UInt8

Adds two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

def

Int8.add (a b : Int8) : Int8

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

UInt16.add (a b : UInt16) : UInt16

Adds two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

def

Int16.add (a b : Int16) : Int16

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

UInt32.add (a b : UInt32) : UInt32

Adds two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

def

Int32.add (a b : Int32) : Int32

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

UInt64.add (a b : UInt64) : UInt64

Adds two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

def

Int64.add (a b : Int64) : Int64

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

USize.sub (a b : USize) : USize

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

ISize.sub (a b : ISize) : ISize

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

UInt8.sub (a b : UInt8) : UInt8

Subtracts one 8-bit unsigned integer from another, wrapping around on underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

def

Int8.sub (a b : Int8) : Int8

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

UInt16.sub (a b : UInt16) : UInt16

Subtracts one 16-bit unsigned integer from another, wrapping around on underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

def

Int16.sub (a b : Int16) : Int16

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

UInt32.sub (a b : UInt32) : UInt32

Subtracts one 32-bit unsigned integer from another, wrapping around on underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

def

Int32.sub (a b : Int32) : Int32

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

UInt64.sub (a b : UInt64) : UInt64

Subtracts one 64-bit unsigned integer from another, wrapping around on underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

def

Int64.sub (a b : Int64) : Int64

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

USize.mul (a b : USize) : USize

Multiplies two word-sized unsigned integers, wrapping around on overflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

def

ISize.mul (a b : ISize) : ISize

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

UInt8.mul (a b : UInt8) : UInt8

Multiplies two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

def

Int8.mul (a b : Int8) : Int8

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

UInt16.mul (a b : UInt16) : UInt16

Multiplies two 16-bit unsigned integers, wrapping around on overflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

def

Int16.mul (a b : Int16) : Int16

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

UInt32.mul (a b : UInt32) : UInt32

Multiplies two 32-bit unsigned integers, wrapping around on overflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

def

Int32.mul (a b : Int32) : Int32

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

UInt64.mul (a b : UInt64) : UInt64

Multiplies two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

def

Int64.mul (a b : Int64) : Int64

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

USize.div (a b : USize) : USize

Unsigned division for word-sized unsigned integers, discarding the remainder. Usually accessed via the / operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

def

ISize.div (a b : ISize) : ISize

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:

ISize.div 10 3 = 3
ISize.div 10 (-3) = (-3)
ISize.div (-10) (-3) = 3
ISize.div (-10) 3 = (-3)
ISize.div 10 0 = 0

def

UInt8.div (a b : UInt8) : UInt8

Unsigned division for 8-bit unsigned integers, discarding the remainder. Usually accessed via the / operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

def

Int8.div (a b : Int8) : Int8

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:

Int8.div 10 3 = 3
Int8.div 10 (-3) = (-3)
Int8.div (-10) (-3) = 3
Int8.div (-10) 3 = (-3)
Int8.div 10 0 = 0

def

UInt16.div (a b : UInt16) : UInt16

Unsigned division for 16-bit unsigned integers, discarding the remainder. Usually accessed via the / operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

def

Int16.div (a b : Int16) : Int16

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:

Int16.div 10 3 = 3
Int16.div 10 (-3) = (-3)
Int16.div (-10) (-3) = 3
Int16.div (-10) 3 = (-3)
Int16.div 10 0 = 0

def

UInt32.div (a b : UInt32) : UInt32

Unsigned division for 32-bit unsigned integers, discarding the remainder. Usually accessed via the / operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

def

Int32.div (a b : Int32) : Int32

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:

Int32.div 10 3 = 3
Int32.div 10 (-3) = (-3)
Int32.div (-10) (-3) = 3
Int32.div (-10) 3 = (-3)
Int32.div 10 0 = 0

def

UInt64.div (a b : UInt64) : UInt64

Unsigned division for 64-bit unsigned integers, discarding the remainder. Usually accessed via the / operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

def

Int64.div (a b : Int64) : Int64

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:

Int64.div 10 3 = 3
Int64.div 10 (-3) = (-3)
Int64.div (-10) (-3) = 3
Int64.div (-10) 3 = (-3)
Int64.div 10 0 = 0

def

USize.mod (a b : USize) : USize

The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one integer by another. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

USize.mod 5 2 = 1
USize.mod 4 2 = 0
USize.mod 4 0 = 4

def

ISize.mod (a b : ISize) : ISize

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:

ISize.mod 5 2 = 1
ISize.mod 5 (-2) = 1
ISize.mod (-5) 2 = (-1)
ISize.mod (-5) (-2) = (-1)
ISize.mod 4 2 = 0
ISize.mod 4 (-2) = 0
ISize.mod 4 0 = 4
ISize.mod (-4) 0 = (-4)

def

UInt8.mod (a b : UInt8) : UInt8

The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one integer by another. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

UInt8.mod 5 2 = 1
UInt8.mod 4 2 = 0
UInt8.mod 4 0 = 4

def

Int8.mod (a b : Int8) : Int8

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:

Int8.mod 5 2 = 1
Int8.mod 5 (-2) = 1
Int8.mod (-5) 2 = (-1)
Int8.mod (-5) (-2) = (-1)
Int8.mod 4 2 = 0
Int8.mod 4 (-2) = 0
Int8.mod 4 0 = 4
Int8.mod (-4) 0 = (-4)

def

UInt16.mod (a b : UInt16) : UInt16

The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one integer by another. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

UInt16.mod 5 2 = 1
UInt16.mod 4 2 = 0
UInt16.mod 4 0 = 4

def

Int16.mod (a b : Int16) : Int16

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:

Int16.mod 5 2 = 1
Int16.mod 5 (-2) = 1
Int16.mod (-5) 2 = (-1)
Int16.mod (-5) (-2) = (-1)
Int16.mod 4 2 = 0
Int16.mod 4 (-2) = 0
Int16.mod 4 0 = 4
Int16.mod (-4) 0 = (-4)

def

UInt32.mod (a b : UInt32) : UInt32

The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one integer by another. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

UInt32.mod 5 2 = 1
UInt32.mod 4 2 = 0
UInt32.mod 4 0 = 4

def

Int32.mod (a b : Int32) : Int32

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:

Int32.mod 5 2 = 1
Int32.mod 5 (-2) = 1
Int32.mod (-5) 2 = (-1)
Int32.mod (-5) (-2) = (-1)
Int32.mod 4 2 = 0
Int32.mod 4 (-2) = 0
Int32.mod 4 0 = 4
Int32.mod (-4) 0 = (-4)

def

UInt64.mod (a b : UInt64) : UInt64

The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one integer by another. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

UInt64.mod 5 2 = 1
UInt64.mod 4 2 = 0
UInt64.mod 4 0 = 4

def

Int64.mod (a b : Int64) : Int64

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:

Int64.mod 5 2 = 1
Int64.mod 5 (-2) = 1
Int64.mod (-5) 2 = (-1)
Int64.mod (-5) (-2) = (-1)
Int64.mod 4 2 = 0
Int64.mod 4 (-2) = 0
Int64.mod 4 0 = 4
Int64.mod (-4) 0 = (-4)

def

USize.log2 (a : USize) : USize

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

def

UInt8.log2 (a : UInt8) : UInt8

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

def

UInt16.log2 (a : UInt16) : UInt16

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

def

UInt32.log2 (a : UInt32) : UInt32

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

def

UInt64.log2 (a : UInt64) : UInt64

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

def

ISize.abs (a : ISize) : ISize

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

Int8.abs (a : Int8) : Int8

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

Int16.abs (a : Int16) : Int16

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

Int32.abs (a : Int32) : Int32

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

Int64.abs (a : Int64) : Int64

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.

18.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 Xor.

def

USize.land (a b : USize) : USize

Bitwise and for word-sized unsigned integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

ISize.land (a b : ISize) : ISize

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

UInt8.land (a b : UInt8) : UInt8

Bitwise and for 8-bit unsigned integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int8.land (a b : Int8) : Int8

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

UInt16.land (a b : UInt16) : UInt16

Bitwise and for 16-bit unsigned integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int16.land (a b : Int16) : Int16

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

UInt32.land (a b : UInt32) : UInt32

Bitwise and for 32-bit unsigned integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int32.land (a b : Int32) : Int32

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

UInt64.land (a b : UInt64) : UInt64

Bitwise and for 64-bit unsigned integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int64.land (a b : Int64) : Int64

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

USize.lor (a b : USize) : USize

Bitwise or for word-sized unsigned integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

ISize.lor (a b : ISize) : ISize

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

UInt8.lor (a b : UInt8) : UInt8

Bitwise or for 8-bit unsigned integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int8.lor (a b : Int8) : Int8

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

UInt16.lor (a b : UInt16) : UInt16

Bitwise or for 16-bit unsigned integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int16.lor (a b : Int16) : Int16

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

UInt32.lor (a b : UInt32) : UInt32

Bitwise or for 32-bit unsigned integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int32.lor (a b : Int32) : Int32

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

UInt64.lor (a b : UInt64) : UInt64

Bitwise or for 64-bit unsigned integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int64.lor (a b : Int64) : Int64

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

USize.xor (a b : USize) : USize

Bitwise exclusive or for word-sized unsigned integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

ISize.xor (a b : ISize) : ISize

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

UInt8.xor (a b : UInt8) : UInt8

Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int8.xor (a b : Int8) : Int8

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

UInt16.xor (a b : UInt16) : UInt16

Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int16.xor (a b : Int16) : Int16

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

UInt32.xor (a b : UInt32) : UInt32

Bitwise exclusive or for 32-bit unsigned integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int32.xor (a b : Int32) : Int32

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

UInt64.xor (a b : UInt64) : UInt64

Bitwise exclusive or for 64-bit unsigned integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.

def

Int64.xor (a b : Int64) : Int64

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

USize.complement (a : USize) : USize

Bitwise complement, also known as bitwise negation, for word-sized unsigned integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.

def

ISize.complement (a : ISize) : ISize

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

UInt8.complement (a : UInt8) : UInt8

Bitwise complement, also known as bitwise negation, for 8-bit unsigned integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.

def

Int8.complement (a : Int8) : Int8

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

UInt16.complement (a : UInt16) : UInt16

Bitwise complement, also known as bitwise negation, for 16-bit unsigned integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.

def

Int16.complement (a : Int16) : Int16

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

UInt32.complement (a : UInt32) : UInt32

Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.

def

Int32.complement (a : Int32) : Int32

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

UInt64.complement (a : UInt64) : UInt64

Bitwise complement, also known as bitwise negation, for 64-bit unsigned integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.

def

Int64.complement (a : Int64) : Int64

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

USize.shiftLeft (a b : USize) : USize

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

This function is overridden at runtime with an efficient implementation.

def

ISize.shiftLeft (a b : ISize) : ISize

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

UInt8.shiftLeft (a b : UInt8) : UInt8

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

This function is overridden at runtime with an efficient implementation.

def

Int8.shiftLeft (a b : Int8) : Int8

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

UInt16.shiftLeft (a b : UInt16) : UInt16

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

This function is overridden at runtime with an efficient implementation.

def

Int16.shiftLeft (a b : Int16) : Int16

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

UInt32.shiftLeft (a b : UInt32) : UInt32

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

This function is overridden at runtime with an efficient implementation.

def

Int32.shiftLeft (a b : Int32) : Int32

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

UInt64.shiftLeft (a b : UInt64) : UInt64

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

This function is overridden at runtime with an efficient implementation.

def

Int64.shiftLeft (a b : Int64) : Int64

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

USize.shiftRight (a b : USize) : USize

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

This function is overridden at runtime with an efficient implementation.

def

ISize.shiftRight (a b : ISize) : ISize

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

UInt8.shiftRight (a b : UInt8) : UInt8

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

This function is overridden at runtime with an efficient implementation.

def

Int8.shiftRight (a b : Int8) : Int8

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

UInt16.shiftRight (a b : UInt16) : UInt16

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

This function is overridden at runtime with an efficient implementation.

def

Int16.shiftRight (a b : Int16) : Int16

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

UInt32.shiftRight (a b : UInt32) : UInt32

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

This function is overridden at runtime with an efficient implementation.

def

Int32.shiftRight (a b : Int32) : Int32

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

UInt64.shiftRight (a b : UInt64) : UInt64

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

This function is overridden at runtime with an efficient implementation.

def

Int64.shiftRight (a b : Int64) : Int64

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.

18.4. Fixed-Precision Integers🔗

18.4.1. Logical Model

18.4.1.1. Unsigned

Constructor

Fields

Constructor

Fields

Constructor

Fields

Constructor

Fields

Constructor

Fields

18.4.1.2. Signed

Fields

Fields

Fields

Fields

Fields

18.4.2. Run-Time Representation

18.4.3. Syntax

18.4.4. API Reference

18.4.4.1. Sizes

18.4.4.2. Ranges

18.4.4.3. Conversions

18.4.4.3.1. To and From Int

18.4.4.3.2. To and From Nat

18.4.4.3.3. To Other Fixed-Width Integers

18.4.4.3.4. To Floating-Point Numbers

18.4.4.3.5. To and From Bitvectors

18.4.4.3.6. To and From Finite Numbers

18.4.4.3.7. To Characters

18.4.4.4. Comparisons🔗

18.4.4.5. Arithmetic🔗

18.4.4.6. Bitwise Operations

18.4.4.3.1. To and From `Int`

18.4.4.3.2. To and From `Nat`