Lean 的标准库包含通常的各种固定宽度整数类型。 从形式化和证明的角度来看，这些类型是适当大小的位向量的包装器；这些包装器确保应用正确的算术操作等实现。 在编译后的代码中，它们的表示非常高效：编译器对它们有特殊的支持，就像对其他基础类型一样。
固定宽度整数可以是无符号的或有符号的。
此外，它们有五种大小：8 位、16 位、32 位和 64 位，以及当前架构的字长。
在它们的逻辑模型中，无符号整数是包装了适当宽度的 BitVec 的结构体。
有符号整数包装了相应的无符号整数，并使用二进制补码表示。
平台架构字长的无符号整数。
在 32 位架构上，USize 等价于 UInt32。在 64 位机器上，它等价于 UInt64。
构造子
USize.ofBitVec
从 BitVec System.Platform.numBits 创建 USize。此函数会被原生实现覆盖。
字段
toBitVec : BitVec System.Platform.numBits
将 USize 解包为 BitVec System.Platform.numBits。此函数会被原生实现覆盖。
平台架构字长的有符号整数。
在 32 位架构上，ISize 等价于 Int32。在 64 位机器上，它等价于 Int64。编译器对此类型提供特殊支持，因此它可以表示为未装箱的值。
构造子
ISize.ofUSize
字段
toUSize : USize
将平台字长有符号整数转换为作为其二进制补码编码的平台字长无符号整数。
有符号 8 位整数。
编译器对此类型提供特殊支持，因此它可以表示为未装箱的 8 位值。
构造子
Int8.ofUInt8
字段
toUInt8 : UInt8
将 8 位有符号整数转换为作为其二进制补码编码的 8 位无符号整数。
有符号 16 位整数。
编译器对此类型提供特殊支持，因此它可以表示为未装箱的 16 位值。
构造子
Int16.ofUInt16
字段
toUInt16 : UInt16
将 16 位有符号整数转换为作为其二进制补码编码的 16 位无符号整数。
有符号 32 位整数。
编译器对此类型提供特殊支持，因此它可以表示为未装箱的 32 位值。
构造子
Int32.ofUInt32
字段
toUInt32 : UInt32
将 32 位有符号整数转换为作为其二进制补码编码的 32 位无符号整数。
有符号 64 位整数。
编译器对此类型提供特殊支持，因此它可以表示为未装箱的 64 位值。
构造子
Int64.ofUInt64
字段
toUInt64 : UInt64
将 64 位有符号整数转换为作为其二进制补码编码的 64 位无符号整数。
在编译后的代码中，即使上下文要求采用装箱表示，只要某种固定宽度整数类型能装入比平台指针少一位的空间，就始终无需额外分配或间接寻址。
这始终包含 Int8、UInt8、Int16 和 UInt16。
在 64 位架构上，Int32 和 UInt32 也可以在没有指针的情况下表示。
在 32 位架构上，Int32 和 UInt32 需要一个指向堆上对象的指针。
ISize、USize、Int64 和 UInt64 在所有架构上都可能需要指针。
尽管通常情况下一些固定宽度整数类型需要装箱，但编译器能够在仅使用特定固定宽度类型而不是多态的代码路径中，（可能在特化阶段之后）在没有装箱或指针间接寻址的情况下表示它们。
这适用于使用这些类型的大多数实际情况：当已知构造子参数、函数参数、函数返回值或中间结果是固定宽度整数类型时，它们的值将使用相应的无符号固定宽度 C 类型来表示。
Lean 运行时系统包含了在归纳类型的构造子中存储固定宽度整数的原语，并且基本操作是在相应的 C 类型上定义的，因此装箱往往发生在整数计算的“边缘”，而不是针对每个中间结果。
在可能出现其他类型的上下文中，例如像 Array 这样的多态容器的内容，这些类型会被装箱，即使静态地知道一个数组只包含单一的固定宽度整数类型。单态数组类型 ByteArray 避免了对 UInt8 数组的装箱。
Lean 不特化归纳类型或数组的表示。
在 Lean 中检查函数的类型不足以确定固定宽度整数值将如何表示，因为装箱的值不会被急切地取消装箱——例如一个从数组中投影出 Int64 的函数返回的是一个装箱的整数值。
所有的固定宽度整数类型都有 OfNat 实例，这允许在表达式和模式上下文中将数字用作字面量。
有符号类型另外还有 Neg 实例，允许应用求负操作。
对于具有 OfNat 实例的类型，Lean 允许使用十进制和十六进制字面量。
在此示例中，字面量表示法用于定义掩码。
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⟩
溢出其类型精度的字面量将被解释为对精度取模。 对于有符号类型，则按底层的二进制补码表示来解释。
以下声明均为真：
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! 🐙
每个固定宽度整数都有一个大小，这是该类型可以表示的不同值的数量。
这不等同于 C 语言的 sizeof 运算符，后者是用来确定该类型占用多少字节的。
Int 转换将平台字长有符号整数转换为表示同一数值的任意精度整数。
此函数在运行时会被高效实现覆盖。
将8 位有符号整数转换为表示同一数值的任意精度整数。
此函数在运行时会被高效实现覆盖。
将16 位有符号整数转换为表示同一数值的任意精度整数。
此函数在运行时会被高效实现覆盖。
将32 位有符号整数转换为表示同一数值的任意精度整数。
此函数在运行时会被高效实现覆盖。
将64 位有符号整数转换为表示同一数值的任意精度整数。
此函数在运行时会被高效实现覆盖。
将任意精度整数转换为平台字长有符号整数；发生上溢或下溢时回绕。
此函数在运行时会被高效实现覆盖。
将任意精度整数转换为8 位有符号整数；发生上溢或下溢时回绕。
此函数在运行时会被高效实现覆盖。
示例：
Int8.ofInt 48 = 48
Int8.ofInt (-115) = -115
Int8.ofInt (-129) = 127
Int8.ofInt (128) = -128
将任意精度整数转换为16 位有符号整数；发生上溢或下溢时回绕。
此函数在运行时会被高效实现覆盖。
示例：
Int16.ofInt 48 = 48
Int16.ofInt (-129) = -129
Int16.ofInt (128) = 128
Int16.ofInt 70000 = 4464
Int16.ofInt (-40000) = 25536
将任意精度整数转换为32 位有符号整数；发生上溢或下溢时回绕。
此函数在运行时会被高效实现覆盖。
示例：
Int32.ofInt 48 = 48
Int32.ofInt (-129) = -129
Int32.ofInt 70000 = 70000
Int32.ofInt (-40000) = -40000
Int32.ofInt 2147483648 = -2147483648
Int32.ofInt (-2147483649) = 2147483647
将任意精度整数转换为64 位有符号整数；发生上溢或下溢时回绕。
此函数在运行时会被高效实现覆盖。
示例：
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
Nat 转换将任意精度自然数转换为平台字长无符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将任意精度自然数转换为平台字长有符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将自然数转换为8 位无符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
UInt8.ofNat 5 = 5
UInt8.ofNat 255 = 255
UInt8.ofNat 256 = 0
UInt8.ofNat 259 = 3
UInt8.ofNat 32770 = 2
将自然数转换为8 位有符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
Int8.ofNat 53 = 53
Int8.ofNat 127 = 127
Int8.ofNat 128 = -128
Int8.ofNat 255 = -1
将自然数转换为16 位无符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
UInt16.ofNat 5 = 5
UInt16.ofNat 255 = 255
UInt16.ofNat 32770 = 32770
UInt16.ofNat 65537 = 1
将自然数转换为16 位有符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
Int16.ofNat 127 = 127
Int16.ofNat 32767 = 32767
Int16.ofNat 32768 = -32768
Int16.ofNat 32770 = -32766
将自然数转换为32 位无符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
UInt32.ofNat 5 = 5
UInt32.ofNat 65539 = 65539
UInt32.ofNat 4_294_967_299 = 3
将自然数转换为32 位有符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
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
将自然数转换为64 位无符号整数；发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
示例：
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
将自然数转换为 64 位有符号整数；发生溢出时回绕为负数。
此函数在运行时会被高效实现覆盖。
示例：
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
将自然数转换为 2^8。需要证明该数足够小，因而可以无溢出地表示。
此函数在运行时会被高效实现覆盖。
将自然数转换为 2^16。需要证明该数足够小，因而可以无溢出地表示。
此函数在运行时会被高效实现覆盖。
将自然数转换为 2^32。需要证明该数足够小，因而可以无溢出地表示。
此函数在运行时会被高效实现覆盖。
将自然数转换为 2^64。需要证明该数足够小，因而可以无溢出地表示。
此函数在运行时会被高效实现覆盖。
将自然数转换为 USize；若该数过大，则返回可表示的最大值。
返回 USize.size - 1；依平台而定，该值为 2^64 - 1 或 2^32 - 1。这适用于大于等于 USize.size 的自然数。
将自然数转换为8 位无符号整数；若该数过大，则返回可表示的最大值。
对于过大的自然数返回 2^8 - 1；这适用于大于等于 2^8 的自然数。
将自然数转换为16 位无符号整数；若该数过大，则返回可表示的最大值。
对于过大的自然数返回 2^16 - 1；这适用于大于等于 2^16 的自然数。
将自然数转换为32 位无符号整数；若该数过大，则返回可表示的最大值。
对于过大的自然数返回 2^32 - 1；这适用于大于等于 2^32 的自然数。
将自然数转换为64 位无符号整数；若该数过大，则返回可表示的最大值。
对于过大的自然数返回 2^64 - 1；这适用于大于等于 2^64 的自然数。
将16 位无符号整数转换为任意精度自然数。
此函数在运行时会被高效实现覆盖。
将32 位无符号整数转换为任意精度自然数。
此函数在运行时会被高效实现覆盖。
将64 位无符号整数转换为任意精度自然数。
此函数在运行时会被高效实现覆盖。
将平台字长无符号整数转换为8 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将平台字长无符号整数转换为16 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将平台字长无符号整数转换为32 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将8 位无符号整数转换为16 位无符号整数。
此函数在运行时会被高效实现覆盖。
将8 位无符号整数转换为32 位无符号整数。
此函数在运行时会被高效实现覆盖。
将8 位无符号整数转换为64 位无符号整数。
此函数在运行时会被高效实现覆盖。
将8 位无符号整数转换为平台字长无符号整数。
此函数在运行时会被高效实现覆盖。
将16 位无符号整数转换为8 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将16 位无符号整数转换为32 位无符号整数。
此函数在运行时会被高效实现覆盖。
将16 位无符号整数转换为64 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将16 位无符号整数转换为平台字长无符号整数。
此函数在运行时会被高效实现覆盖。
将32 位无符号整数转换为8 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将32 位无符号整数转换为16 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将32 位无符号整数转换为64 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将32 位无符号整数转换为平台字长无符号整数。
此函数在运行时会被高效实现覆盖。
将64 位无符号整数转换为8 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将64 位无符号整数转换为16 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
将64 位无符号整数转换为32 位无符号整数。发生溢出时回绕。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将平台字长有符号整数转换为8 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将平台字长有符号整数转换为16 位有符号整数。
此函数在运行时会被高效实现覆盖。
将平台字长有符号整数转换为 32 位有符号整数。
在 32 位平台上，此转换不会损失信息。在 64 位平台上，该整数的位向量表示会被截断为 32 位。此函数在运行时会被高效实现覆盖。
此函数在运行时会被高效实现覆盖。
将8 位有符号整数转换为表示同一数值的16 位有符号整数。
此函数在运行时会被高效实现覆盖。
将8 位有符号整数转换为表示同一数值的32 位有符号整数。
此函数在运行时会被高效实现覆盖。
将8 位有符号整数转换为表示同一数值的64 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将16 位有符号整数转换为8 位有符号整数。
此函数在运行时会被高效实现覆盖。
将16 位有符号整数转换为表示同一数值的32 位有符号整数。
此函数在运行时会被高效实现覆盖。
将16 位有符号整数转换为表示同一数值的64 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将32 位有符号整数转换为8 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将32 位有符号整数转换为16 位有符号整数。
此函数在运行时会被高效实现覆盖。
将32 位有符号整数转换为表示同一数值的64 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将64 位有符号整数转换为8 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将64 位有符号整数转换为16 位有符号整数。
此函数在运行时会被高效实现覆盖。
通过截断位向量表示，将64 位有符号整数转换为32 位有符号整数。
此函数在运行时会被高效实现覆盖。
将 64 位有符号整数转换为平台字长有符号整数；在 32 位平台上会截断其位向量表示，在 64 位平台上则不会损失信息。
此函数在运行时会被高效实现覆盖。
将平台字长无符号整数转换为十进制字符串。
此函数在运行时会被高效实现覆盖。
示例：
USize.repr 0 = "0"
USize.repr 28 = "28"
USize.repr 307 = "307"
Char 类型是对 UInt32 的包装器，它需要一个证明，证明所包装的整数表示一个 Unicode 代码点。
该谓词是 UInt32 API 的一部分。
本节中的运算符很少通过名称调用。
通常，定宽整数上的比较操作应该使用相应关系的可判定性，这些关系由相等类型 Eq 以及在 LE 和 LT 实例中实现的关系组成。
字大小无符号整数的非严格不等式，定义为相应自然数的不等式。通常通过 ≤ 运算符访问。
字长有符号整数的非严格不等式，定义为相应整数的不等式。通常通过 ≤ 运算符访问。
8 位无符号整数的非严格不等式，定义为相应自然数的不等式。通常通过 ≤ 运算符访问。
16 位无符号整数的非严格不等式，定义为相应自然数的不等式。通常通过 ≤ 运算符访问。
16 位有符号整数的非严格不等式，定义为相应整数的不等式。通常通过 ≤ 运算符访问。
32 位无符号整数的非严格不等式，定义为相应自然数的不等式。通常通过 ≤ 运算符访问。
32 位有符号整数的非严格不等式，定义为相应整数的不等式。通常通过 ≤ 运算符访问。
64 位无符号整数的非严格不等式，定义为相应自然数的不等式。通常通过 ≤ 运算符访问。
64 位有符号整数的非严格不等式，定义为相应整数的不等式。通常通过 ≤ 运算符访问。
字长无符号整数的严格不等式，定义为相应自然数的不等式。通常通过 < 运算符访问。
字长有符号整数的严格不等式，定义为相应整数的不等式。通常通过 < 运算符访问。
8 位无符号整数的严格不等式，定义为相应自然数的不等式。通常通过 < 运算符访问。
16位无符号整数的严格不等式，定义为相应自然数的不等式。通常通过 < 运算符访问。
16 位有符号整数的严格不等式，定义为相应整数的不等式。通常通过 < 运算符访问。
32位无符号整数的严格不等式，定义为相应自然数的不等式。通常通过 < 运算符访问。
32 位有符号整数的严格不等式，定义为相应整数的不等式。通常通过 < 运算符访问。
64位无符号整数的严格不等式，定义为相应自然数的不等式。通常通过 < 运算符访问。
64 位有符号整数的严格不等式，定义为相应整数的不等式。通常通过 < 运算符访问。
通常，定宽整数上的算术运算应通过 Lean 的重载算术记号来使用，尤其是它们的 Add、Sub、Mul、Div 与 Mod 实例，以及有符号类型的 Neg 实例。
对字长有符号整数取负。通常通过前缀运算符 - 使用。
此函数在运行时会被高效实现覆盖。
对16 位有符号整数取负。通常通过前缀运算符 - 使用。
此函数在运行时会被高效实现覆盖。
对32 位有符号整数取负。通常通过前缀运算符 - 使用。
此函数在运行时会被高效实现覆盖。
对64 位有符号整数取负。通常通过前缀运算符 - 使用。
此函数在运行时会被高效实现覆盖。
对64 位无符号整数取负，结果按 UInt64.size 取模。
UInt64.neg a 等价于 18_446_744_073_709_551_615 - a + 1。
此函数在运行时会被高效实现覆盖。
将两个字长无符号整数相加，在溢出时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个字长有符号整数相加，在溢出或下溢时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个8 位无符号整数相加，在溢出时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个8 位有符号整数相加，在溢出或下溢时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个16 位无符号整数相加，在溢出时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个16 位有符号整数相加，在溢出或下溢时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个32 位无符号整数相加，在溢出时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个32 位有符号整数相加，在溢出或下溢时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个64 位无符号整数相加，在溢出时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个64 位有符号整数相加，在溢出或下溢时回绕。通常通过 + 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个字长无符号整数中减去一个整数，在下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个字长有符号整数中减去一个整数，在溢出或下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个8 位无符号整数中减去一个整数，在下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个8 位有符号整数中减去一个整数，在溢出或下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个16 位无符号整数中减去一个整数，在下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个16 位有符号整数中减去一个整数，在溢出或下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个32 位无符号整数中减去一个整数，在下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个32 位有符号整数中减去一个整数，在溢出或下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个64 位无符号整数中减去一个整数，在下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
从另一个64 位有符号整数中减去一个整数，在溢出或下溢时回绕。通常通过 - 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个字长无符号整数相乘，在溢出时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个字长有符号整数相乘，在溢出或下溢时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个8 位无符号整数相乘，在溢出时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个8 位有符号整数相乘，在溢出或下溢时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个16 位无符号整数相乘，在溢出时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个16 位有符号整数相乘，在溢出或下溢时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个32 位无符号整数相乘，在溢出时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个32 位有符号整数相乘，在溢出或下溢时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个64 位无符号整数相乘，在溢出时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
将两个64 位有符号整数相乘，在溢出或下溢时回绕。通常通过 * 运算符使用。
此函数在运行时会被高效实现覆盖。
字长无符号整数的无符号除法，舍弃余数。通常通过 / 运算符使用。
此操作有时称为“向下取整除法”。除以零的结果定义为零。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的无符号除法，舍弃余数。通常通过 / 运算符使用。
此操作有时称为“向下取整除法”。除以零的结果定义为零。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的无符号除法，舍弃余数。通常通过 / 运算符使用。
此操作有时称为“向下取整除法”。除以零的结果定义为零。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的无符号除法，舍弃余数。通常通过 / 运算符使用。
此操作有时称为“向下取整除法”。除以零的结果定义为零。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的无符号除法，舍弃余数。通常通过 / 运算符使用。
此操作有时称为“向下取整除法”。除以零的结果定义为零。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的取模运算，计算一个整数除以另一个整数的余数。通常通过 % 运算符使用。
当除数为 0 时，结果为被除数，而不是报错。
此函数在运行时会被高效实现覆盖。
示例：
UInt16.mod 5 2 = 1
UInt16.mod 4 2 = 0
UInt16.mod 4 0 = 4
32 位无符号整数的取模运算，计算一个整数除以另一个整数的余数。通常通过 % 运算符使用。
当除数为 0 时，结果为被除数，而不是报错。
此函数在运行时会被高效实现覆盖。
示例：
UInt32.mod 5 2 = 1
UInt32.mod 4 2 = 0
UInt32.mod 4 0 = 4
64 位无符号整数的取模运算，计算一个整数除以另一个整数的余数。通常通过 % 运算符使用。
当除数为 0 时，结果为被除数，而不是报错。
此函数在运行时会被高效实现覆盖。
示例：
UInt64.mod 5 2 = 1
UInt64.mod 4 2 = 0
UInt64.mod 4 0 = 4
字长无符号整数的以 2 为底的对数。返回 ⌊max 0 (log₂ a)⌋。
此函数在运行时会被高效实现覆盖。此定义是其逻辑模型。
示例：
USize.log2 0 = 0
USize.log2 1 = 0
USize.log2 2 = 1
USize.log2 4 = 2
USize.log2 7 = 2
USize.log2 8 = 3
8 位无符号整数的以 2 为底的对数。返回 ⌊max 0 (log₂ a)⌋。
此函数在运行时会被高效实现覆盖。此定义是其逻辑模型。
示例：
UInt8.log2 0 = 0
UInt8.log2 1 = 0
UInt8.log2 2 = 1
UInt8.log2 4 = 2
UInt8.log2 7 = 2
UInt8.log2 8 = 3
16 位无符号整数的以 2 为底的对数。返回 ⌊max 0 (log₂ a)⌋。
此函数在运行时会被高效实现覆盖。此定义是其逻辑模型。
示例：
UInt16.log2 0 = 0
UInt16.log2 1 = 0
UInt16.log2 2 = 1
UInt16.log2 4 = 2
UInt16.log2 7 = 2
UInt16.log2 8 = 3
32 位无符号整数的以 2 为底的对数。返回 ⌊max 0 (log₂ a)⌋。
此函数在运行时会被高效实现覆盖。此定义是其逻辑模型。
示例：
UInt32.log2 0 = 0
UInt32.log2 1 = 0
UInt32.log2 2 = 1
UInt32.log2 4 = 2
UInt32.log2 7 = 2
UInt32.log2 8 = 3
64 位无符号整数的以 2 为底的对数。返回 ⌊max 0 (log₂ a)⌋。
此函数在运行时会被高效实现覆盖。此定义是其逻辑模型。
示例：
UInt64.log2 0 = 0
UInt64.log2 1 = 0
UInt64.log2 2 = 1
UInt64.log2 4 = 2
UInt64.log2 7 = 2
UInt64.log2 8 = 3
计算字长有符号整数的绝对值。
此函数等价于 if a < 0 then -a else a，因此特别地，ISize.minValue 会映射到 ISize.minValue。
此函数在运行时会被高效实现覆盖。
计算8 位有符号整数的绝对值。
此函数等价于 if a < 0 then -a else a，因此特别地，Int8.minValue 会映射到 Int8.minValue。
此函数在运行时会被高效实现覆盖。
计算16 位有符号整数的绝对值。
此函数等价于 if a < 0 then -a else a，因此特别地，Int16.minValue 会映射到 Int16.minValue。
此函数在运行时会被高效实现覆盖。
计算32 位有符号整数的绝对值。
此函数等价于 if a < 0 then -a else a，因此特别地，Int32.minValue 会映射到 Int32.minValue。
此函数在运行时会被高效实现覆盖。
通常，对固定宽度整数的按位操作应该使用 Lean 的重载运算符来访问，特别是它们对 ShiftLeft、ShiftRight、AndOp、OrOp 和 XorOp 的实例。
平台字长无符号整数的按位与。通常通过 &&& 运算符访问。
仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
平台字长有符号整数的按位与。通常通过 &&& 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的按位与。通常通过 &&& 运算符访问。
仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
8 位有符号整数的按位与。通常通过 &&& 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的按位与。通常通过 &&& 运算符访问。
仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
16 位有符号整数的按位与。通常通过 &&& 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的按位与。通常通过 &&& 运算符访问。
仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
32 位有符号整数的按位与。通常通过 &&& 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的按位与。通常通过 &&& 运算符访问。
仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
64 位有符号整数的按位与。通常通过 &&& 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位都为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
平台字长无符号整数的按位或。通常通过 ||| 运算符访问。
只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
平台字长有符号整数的按位或。通常通过 ||| 运算符访问。
按照二进制补码表示，只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的按位或。通常通过 ||| 运算符访问。
只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
8 位有符号整数的按位或。通常通过 ||| 运算符访问。
按照二进制补码表示，只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的按位或。通常通过 ||| 运算符访问。
只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
16 位有符号整数的按位或。通常通过 ||| 运算符访问。
按照二进制补码表示，只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的按位或。通常通过 ||| 运算符访问。
只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
32 位有符号整数的按位或。通常通过 ||| 运算符访问。
按照二进制补码表示，只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的按位或。通常通过 ||| 运算符访问。
只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
64 位有符号整数的按位或。通常通过 ||| 运算符访问。
按照二进制补码表示，只要输入整数的对应位中至少有一个为 1，结果整数的该位就为 1。
此函数在运行时会被高效实现覆盖。
平台字长无符号整数的按位异或。通常通过 ^^^ 运算符访问。
仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
平台字长有符号整数的按位异或。通常通过 ^^^ 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的按位异或。通常通过 ^^^ 运算符访问。
仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
8 位有符号整数的按位异或。通常通过 ^^^ 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的按位异或。通常通过 ^^^ 运算符访问。
仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
16 位有符号整数的按位异或。通常通过 ^^^ 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的按位异或。通常通过 ^^^ 运算符访问。
仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
32 位有符号整数的按位异或。通常通过 ^^^ 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的按位异或。通常通过 ^^^ 运算符访问。
仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
64 位有符号整数的按位异或。通常通过 ^^^ 运算符访问。
按照二进制补码表示，仅当两个输入整数的对应位中恰有一个为 1 时，结果整数的该位才为 1。
此函数在运行时会被高效实现覆盖。
平台字长无符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。
此函数在运行时会被高效实现覆盖。
平台字长有符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。整数使用二进制补码表示，因此 ISize.complement a = -(a + 1)。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。
此函数在运行时会被高效实现覆盖。
8 位有符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。整数使用二进制补码表示，因此 Int8.complement a = -(a + 1)。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。
此函数在运行时会被高效实现覆盖。
16 位有符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。整数使用二进制补码表示，因此 Int16.complement a = -(a + 1)。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。
此函数在运行时会被高效实现覆盖。
32 位有符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。整数使用二进制补码表示，因此 Int32.complement a = -(a + 1)。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。
此函数在运行时会被高效实现覆盖。
64 位有符号整数的按位补码（也称按位取反）。通常通过 ~~~ 运算符访问。
结果整数的每一位都与输入整数的对应位相反。整数使用二进制补码表示，因此 Int64.complement a = -(a + 1)。
此函数在运行时会被高效实现覆盖。
平台字长无符号整数的按位左移。通常通过 <<< 运算符访问。
此函数在运行时会被高效实现覆盖。
平台字长有符号整数的按位左移。通常通过 <<< 运算符访问。
有符号整数按照二进制补码表示解释为位向量。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的按位左移。通常通过 <<< 运算符访问。
此函数在运行时会被高效实现覆盖。
8 位有符号整数的按位左移。通常通过 <<< 运算符访问。
有符号整数按照二进制补码表示解释为位向量。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的按位左移。通常通过 <<< 运算符访问。
此函数在运行时会被高效实现覆盖。
16 位有符号整数的按位左移。通常通过 <<< 运算符访问。
有符号整数按照二进制补码表示解释为位向量。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的按位左移。通常通过 <<< 运算符访问。
此函数在运行时会被高效实现覆盖。
32 位有符号整数的按位左移。通常通过 <<< 运算符访问。
有符号整数按照二进制补码表示解释为位向量。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的按位左移。通常通过 <<< 运算符访问。
此函数在运行时会被高效实现覆盖。
64 位有符号整数的按位左移。通常通过 <<< 运算符访问。
有符号整数按照二进制补码表示解释为位向量。
此函数在运行时会被高效实现覆盖。
平台字长无符号整数的按位右移。通常通过 >>> 运算符访问。
此函数在运行时会被高效实现覆盖。
平台字长有符号整数的算术右移。通常通过 <<< 运算符访问。
高位用最高有效位的值填充。
此函数在运行时会被高效实现覆盖。
8 位无符号整数的按位右移。通常通过 >>> 运算符访问。
此函数在运行时会被高效实现覆盖。
8 位有符号整数的算术右移。通常通过 <<< 运算符访问。
高位用最高有效位的值填充。
此函数在运行时会被高效实现覆盖。
16 位无符号整数的按位右移。通常通过 >>> 运算符访问。
此函数在运行时会被高效实现覆盖。
16 位有符号整数的算术右移。通常通过 <<< 运算符访问。
高位用最高有效位的值填充。
此函数在运行时会被高效实现覆盖。
32 位无符号整数的按位右移。通常通过 >>> 运算符访问。
此函数在运行时会被高效实现覆盖。
32 位有符号整数的算术右移。通常通过 <<< 运算符访问。
高位用最高有效位的值填充。
此函数在运行时会被高效实现覆盖。
64 位无符号整数的按位右移。通常通过 >>> 运算符访问。
此函数在运行时会被高效实现覆盖。
64 位有符号整数的算术右移。通常通过 <<< 运算符访问。
高位用最高有效位的值填充。
此函数在运行时会被高效实现覆盖。