Lean 语言参考

20.4. 固定精度整数🔗

Lean 的标准库包括 固定位宽整数 类型的常见分类。 从形式化和证明的角度来看,这些类型是适当大小的位向量的包装器;包装器确保例如的正确实现应用算术运算。 在编译的代码中,它们被有效地表示:编译器对它们有特殊的支持,就像对其他基本类型的支持一样。

20.4.1. 逻辑模型🔗

固定位宽整数 可以是未签名的或已签名的。 此外,它们还有五种大小:8、16、32 和 64 位,以及当前架构的字大小。 在它们的逻辑模型中,无符号整数是包装适当宽度的 BitVec 的结构。 有符号整数包装相应的无符号整数,并使用二进制补码表示形式。

20.4.1.1. 未签名🔗

🔗structure
USize : Type
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
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
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
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
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.

20.4.1.2. 签名🔗

🔗structure
ISize : Type
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.

Constructor

ISize.ofUSize

Fields

toUSize : USize

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

🔗structure
Int8 : Type
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.

Constructor

Int8.ofUInt8

Fields

toUInt8 : UInt8

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

🔗structure
Int16 : Type
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.

Constructor

Int16.ofUInt16

Fields

toUInt16 : UInt16

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

🔗structure
Int32 : Type
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.

Constructor

Int32.ofUInt32

Fields

toUInt32 : UInt32

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

🔗structure
Int64 : Type
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.

Constructor

Int64.ofUInt64

Fields

toUInt64 : UInt64

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

20.4.2. 运行时表示🔗

在需要 boxed 表示的上下文中的编译代码中,始终表示比平台指针大小少一位的 固定位宽整数 类型,而无需额外的分配或间接寻址。 这始终包括 Int8UInt8Int16UInt16。 在 64 位体系结构上,Int32UInt32 也以不带指针的方式表示。 在 32 位体系结构上,Int32UInt32 需要指向堆上对象的指针。 ISizeUSizeInt64UInt64 可能需要所有架构上的指针。

尽管某些固定整数类型通常需要装箱,但编译器能够在仅使用特定固定宽度类型而不是多态的代码路径中表示它们,而无需装箱或指针间接,可能在专门化过程之后。 这适用于使用这些类型的大多数实际情况:当构造函数参数、函数参数、函数返回值或中间结果已知为 固定位宽整数 类型时,它们的值使用相应的无符号固定宽度 C 类型表示。 Lean 运行时系统包括用于在 归纳类型 的构造函数中存储 固定位宽整数 的原语,并且原语操作是在相应的 C 类型上定义的,因此装箱往往发生在整数计算的“边缘”,而不是针对每个中间结果。 在可能出现其他类型的上下文中,例如 Array 等多态容器的内容,即使数组静态已知仅包含单个 固定位宽整数 类型,这些类型也会被装箱。单态数组类型 ByteArray 避免对 UInt8 数组进行装箱。 Lean 不专门表示归纳类型或数组。 检查 Lean 中函数的类型不足以确定如何表示 固定位宽整数 值,因为装箱值不会立即拆箱 — 从数组投影 Int64 的函数会返回装箱整数值。

20.4.3. 句法🔗

所有 固定位宽整数 类型都有 OfNat 实例,这些实例允许在表达式和模式上下文中将数字用作文字。 签名类型还具有 Neg 实例,允许应用否定。

Fixed-Width Literals

Lean 允许将十进制和十六进制文字用于具有 OfNat 实例的类型。 在此示例中,使用文字符号来定义掩码。

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

溢出其类型精度的文字被解释为对精度取模。 有符号类型根据底层的补码表示进行解释。

Overflowing Fixed-Width Literals

以下陈述全部正确:

example : (255 : UInt8) = 255 := 255 = 255 All goals completed! 🐙 example : (256 : UInt8) = 0 := 256 = 0 All goals completed! 🐙 example : (257 : UInt8) = 1 := 257 = 1 All goals completed! 🐙 example : (0x7f : Int8) = 127 := 127 = 127 All goals completed! 🐙 example : (0x8f : Int8) = -113 := 143 = -113 All goals completed! 🐙 example : (0xff : Int8) = -1 := 255 = -1 All goals completed! 🐙

20.4.4. API 参考🔗

20.4.4.1. 尺寸🔗

每个 固定位宽整数 都有一个size,它是该类型可以表示的不同值的数量。 这并不等同于 C 的 sizeof 运算符,而是确定类型占用多少字节。

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

20.4.4.2. 范围🔗

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

20.4.4.3. 转换🔗

20.4.4.3.1. 往返 Int🔗

🔗def

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

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

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

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

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

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

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:

🔗def

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:

🔗def

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:

🔗def

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:

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

20.4.4.3.2. 往返 Nat🔗

🔗def

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

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

Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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:

🔗def

Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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:

🔗def

Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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:

🔗def

Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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:

🔗def
USize.ofNat32 (n : Nat) (h : n < 4294967296) : USize
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

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

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

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

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

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

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

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

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

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

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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.

20.4.4.3.3. 至其他 固定位宽整数🔗

🔗def

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

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

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

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

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

🔗def

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

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

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

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

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

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

🔗def

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

20.4.4.3.4. 转浮点数🔗

🔗opaque

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

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

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

This function does not reduce in the kernel.

🔗opaque

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

This function does not reduce in the kernel.

🔗opaque

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

This function does not reduce in the kernel.

🔗opaque

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

This function does not reduce in the kernel.

🔗opaque

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

This function does not reduce in the kernel.

🔗opaque

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

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

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

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

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

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

🔗opaque

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

🔗opaque

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

🔗opaque

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

🔗opaque

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

🔗opaque

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

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

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.

20.4.4.3.5. 往返位向量🔗

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

🔗def

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

20.4.4.3.6. 有限数的往返🔗

🔗def

Converts a USize into the corresponding Fin USize.size.

🔗def

Converts a UInt8 into the corresponding Fin UInt8.size.

🔗def

Converts a UInt16 into the corresponding Fin UInt16.size.

🔗def

Converts a UInt32 into the corresponding Fin UInt32.size.

🔗def

Converts a UInt64 into the corresponding Fin UInt64.size.

🔗def

Converts a Fin USize.size into the corresponding USize.

🔗def

Converts a Fin UInt8.size into the corresponding UInt8.

🔗def

Converts a Fin UInt16.size into the corresponding UInt16.

🔗def

Converts a Fin UInt32.size into the corresponding UInt32.

🔗def

Converts a Fin UInt64.size into the corresponding UInt64.

🔗def

Converts a word-sized unsigned integer into a decimal string.

This function is overridden at runtime with an efficient implementation.

Examples:

20.4.4.3.7. 致人物🔗

Char 类型是 UInt32 的包装器,需要证明包装的整数表示 Unicode 代码点。 该谓词是 UInt32 API 的一部分。

🔗def

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

20.4.4.4. 比较🔗

本节中的运算符很少按名称调用。 通常,固定位宽整数 上的比较操作应使用相应关系的可判定性,该关系由相等类型 Eq 以及在 LELT 实例中实现的类型组成。

🔗def
USize.le (a b : USize) : Prop
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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

Decides whether two word-sized unsigned integers are equal. Usually accessed via the DecidableEq USize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two word-sized signed integers are equal. Usually accessed via the DecidableEq ISize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 8-bit unsigned integers are equal. Usually accessed via the DecidableEq UInt8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 8-bit signed integers are equal. Usually accessed via the DecidableEq Int8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 16-bit unsigned integers are equal. Usually accessed via the DecidableEq UInt16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 16-bit signed integers are equal. Usually accessed via the DecidableEq Int16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 32-bit unsigned integers are equal. Usually accessed via the DecidableEq UInt32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 32-bit signed integers are equal. Usually accessed via the DecidableEq Int32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 64-bit unsigned integers are equal. Usually accessed via the DecidableEq UInt64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether two 64-bit signed integers are equal. Usually accessed via the DecidableEq Int64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed via the DecidableLE USize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one word-sized signed integer is less than or equal to another. Usually accessed via the DecidableLE ISize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the DecidableLE UInt32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the DecidableLE Int32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via the DecidableLT USize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one word-sized signed integer is strictly less than another. Usually accessed via the DecidableLT ISize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Decides whether one 32-bit signed integer is strictly less than another. Usually accessed via the DecidableLT Int32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

This function is overridden at runtime with an efficient implementation.

Examples:

20.4.4.5. 算术🔗

通常,固定位宽整数 上的算术运算应使用 Lean 的重载算术表示法进行访问,特别是 AddSubMulDivMod 的实例,以及Neg 用于有符号类型。

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Adds two word-sized signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.add (a b : Int8) : Int8
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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Adds two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Adds two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Adds two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Subtracts one word-sized signed integer from another, wrapping around on over- or underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.sub (a b : Int8) : Int8
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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Multiplies two word-sized signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.mul (a b : Int8) : Int8
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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Multiplies two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Multiplies two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Multiplies two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Truncating division for word-sized signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.div (a b : Int8) : Int8
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:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Truncating division for 16-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Truncating division for 32-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Truncating division for 64-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

The modulo operator for word-sized signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by ISize.div. Usually accessed via the % operator.

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def
Int8.mod (a b : Int8) : Int8
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:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

The modulo operator for 16-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int16.div. Usually accessed via the % operator.

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

The modulo operator for 32-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int32.div. Usually accessed via the % operator.

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

The modulo operator for 64-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int64.div. Usually accessed via the % operator.

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

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def

Base-two logarithm of word-sized unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

🔗def

Base-two logarithm of 8-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

🔗def

Base-two logarithm of 16-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

🔗def

Base-two logarithm of 32-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

🔗def

Base-two logarithm of 64-bit unsigned integers. Returns ⌊max 0 (log₂ a)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

🔗def

Computes the absolute value of a word-sized signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular ISize.minValue will be mapped to ISize.minValue.

This function is overridden at runtime with an efficient implementation.

🔗def

Computes the absolute value of an 8-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int8.minValue will be mapped to Int8.minValue.

This function is overridden at runtime with an efficient implementation.

🔗def

Computes the absolute value of a 16-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int16.minValue will be mapped to Int16.minValue.

This function is overridden at runtime with an efficient implementation.

🔗def

Computes the absolute value of a 32-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int32.minValue will be mapped to Int32.minValue.

This function is overridden at runtime with an efficient implementation.

🔗def

Computes the absolute value of a 64-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int64.minValue will be mapped to Int64.minValue.

This function is overridden at runtime with an efficient implementation.

20.4.4.6. 按位运算🔗

通常,应使用 Lean 的重载运算符(特别是 ShiftLeftShiftRightAndOpOrOpXorOp 的实例)访问 固定位宽整数 上的按位运算。

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.land (a b : Int8) : Int8
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

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.lor (a b : Int8) : Int8
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

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def
Int8.xor (a b : Int8) : Int8
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

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

Bitwise exclusive or for 16-bit signed integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so ISize.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int8.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int16.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int32.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

🔗def

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

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int64.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

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

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Arithmetic right shift for word-sized signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Arithmetic right shift for 8-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Arithmetic right shift for 16-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Arithmetic right shift for 32-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

🔗def

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

This function is overridden at runtime with an efficient implementation.

🔗def

Arithmetic right shift for 64-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.