Float 类型的逻辑模型。

它定义为 UInt64 的一种类型，并附加限制：编码 NaN 的位模式必须恰好是选定的规范 NaN。

大多数 Float.Model 函数会先把 Float.Model 解包为归纳类型 UnpackedFloat，在那里执行运算，然后把结果重新打包成 Float.Model。

本开发并不以成为通用浮点数库的基础为目标，也不打算直接为它编写任何引理。希望获得浮点数库的用户应完全独立地开发这样的库；希望证明涉及 Float 的程序性质的用户，则应证明此处定义的运算等价于独立库中定义的运算，再把该库的引理转移到 Float 和 Float32 类型上。

Float.Model.mk

toBits : UInt64

valid : Float.Model.Format.binary64.Valid self.toBits.toBitVec

Float32 类型的逻辑模型。

它定义为 UInt32 的一种类型，并附加限制：编码 NaN 的位模式必须恰好是选定的规范 NaN。

大多数 Float32.Model 函数会先把 Float32.Model 解包为归纳类型 UnpackedFloat，在那里执行运算，然后把结果重新打包成 Float32.Model。

本开发并不以成为通用浮点数库的基础为目标，也不打算直接为它编写任何引理。希望获得浮点数库的用户应完全独立地开发这样的库；希望证明涉及 Float32 的程序性质的用户，则应证明此处定义的运算等价于独立库中定义的运算，再把该库的引理转移到 Float 和 Float32 类型上。

Float32.Model.mk

toBits : UInt32

valid : Float.Model.Format.binary32.Valid self.toBits.toBitVec

把 UnpackedFloat 打包为相应的 Float.Model。 只有当该浮点数已经按 Format.binary64 格式正确舍入时，此运算的结果才有意义。

把 UnpackedFloat 打包为相应的 Float32.Model。 只有当该浮点数已经按 Format.binary32 格式正确舍入时，此运算的结果才有意义。

把 Float.Model 解包为相应的 UnpackedFloat。

把 Float32.Model 解包为相应的 UnpackedFloat。

一种表示浮点数的归纳类型，其构造子分别表示带符号无穷、不带载荷的非数、带符号零，以及由符号、正自然数尾数和整数指数构成的有限浮点数。

有限浮点数在此格式中没有唯一表示：尾数乘以二、指数减一后，所得有限浮点数仍表示同一个有理数。

对于给定的 Format，若指数等于该格式规定的 targetExponent，就称解包后的浮点数处于规范形式。UnpackedFloat 上的某些运算（例如 compare）假定所有输入都对同一格式处于规范形式。

请注意，对给定格式处于规范形式的解包浮点数未必能由该格式实际表示，因为指数可能太大而无法容纳。此时，pack 函数会使浮点数上溢为无穷。

此类型仅用于支持 Float.Model 和 Float32.Model。本开发并不以成为通用浮点数库的基础为目标，也不打算直接为它编写任何引理。希望获得浮点数库的用户应完全独立地开发这样的库；希望证明涉及 Float 的程序性质的用户，则应证明此处定义的运算等价于独立库中定义的运算，再把该库的引理转移到 Float 和 Float32 类型上。

Float.Model.UnpackedFloat.infinity
  (sign : Float.Model.UnpackedFloat.Sign) :
  Float.Model.UnpackedFloat

Float.Model.UnpackedFloat.notANumber :
  Float.Model.UnpackedFloat

Float.Model.UnpackedFloat.zero
  (sign : Float.Model.UnpackedFloat.Sign) :
  Float.Model.UnpackedFloat

Float.Model.UnpackedFloat.finite
  (sign : Float.Model.UnpackedFloat.Sign) (mantissa : Nat)
  (exponent : Int) (mantissa_pos : 0 < mantissa) :
  Float.Model.UnpackedFloat

计算两个浮点数之和，并按照给定规约舍入结果。

计算两个浮点数之差，并按照给定规约舍入结果。

计算两个浮点数之积，并按照给定规约舍入结果。

计算两个浮点数之商，并按照给定规约舍入结果。

计算浮点数的平方根，并按照给定规约舍入结果。

对给定浮点数取负。

返回具有正号的给定浮点数。

返回 true，当且仅当该浮点数为 NaN。

若该浮点数为正无穷或负无穷，则返回 true。

返回 true，当该浮点数表示实数，即它既非无穷也非 NaN。

按照 IEEE 规定计算两个浮点数的次序。返回 Option Ordering，以体现 NaN 与任何值都不可比较这一事实。正零与负零也视为相等。

重要：仅当两个输入都对同一格式处于规范形式时，此运算才能正确工作（详情参见 UnpackedFloat 的文档字符串）。

按照 IEEE 规则判断 a 是否等于 b。

该关系不具自反性。

按照 IEEE 规则判断 a 是否小于 b。

这不是全序。

按照 IEEE 规则判断 a 是否小于或等于 b。

这不是全序，并且 ≤ 不具自反性。

把 Nat 转换为 UnpackedFloat；输入为零时返回正零。

把 Int 转换为 UnpackedFloat；输入为零时返回正零。

计算 m * 10 ^ e。

把 UnpackedFloat 转换为 Int8：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 Int8 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 Int16：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 Int16 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 Int32：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 Int32 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 Int64：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 Int64 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 ISize：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 ISize 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 UInt8：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 UInt8 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 UInt16：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 UInt16 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 UInt32：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 UInt32 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 UInt64：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 UInt64 转换为 UnpackedFloat；输入为零时返回正零。

把 UnpackedFloat 转换为 USize：截去小数点后的部分，把 NaN 转换为 0，并将越界值和无穷值钳制到范围内。

把 USize 转换为 UnpackedFloat；输入为零时返回正零。

检查浮点数是否为正无穷或负无穷，而不是有限数或 NaN。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 运算符 isinf。

检查浮点数是否为正无穷或负无穷，而不是有限数或 NaN。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 运算符 isinf。

检查浮点数是否为 NaN（“非数”）值。

NaN 值由原本可能成为错误的运算产生，例如零除以零。

此函数返回 true 当且仅当输入在命题上等于 Float.nan。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 运算符 isnan。

检查浮点数是否为 NaN（“非数”）值。

NaN 值由原本可能成为错误的运算产生，例如零除以零。

此函数返回 true 当且仅当输入在命题上等于 Float32.nan。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 运算符 isnan。

检查浮点数是否有限，即它是正规数、次正规数或零，而不是无穷或 NaN。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 运算符 isfinite。

检查浮点数是否有限，即它是正规数、次正规数或零，而不是无穷或 NaN。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 运算符 isfinite。

逐位转换为 UInt64。把 Float 解释为 UInt64，忽略数值，仅将 Float 的位模式视为 UInt64。

在所有受支持平台上，Float 与 UInt64 的字节序相同。IEEE 754 非常精确地规定了浮点数的位布局。

此函数不同于 Float.toUInt64；后者试图保持数值，而不是重新解释位模式。

逐位转换为 UInt32。把 Float32 解释为 UInt32，忽略数值，仅将 Float32 的位模式视为 UInt32。

在所有受支持平台上，Float32 与 UInt32 的字节序相同。IEEE 754 非常精确地规定了浮点数的位布局。

此函数不同于 Float.toUInt32；后者试图保持数值，而不是重新解释位模式。

从 UInt64 逐位转换。把 UInt64 解释为 Float，忽略数值，仅将 UInt64 的位模式视为 Float。

在所有受支持平台上，Float 与 UInt64 的字节序相同。IEEE 754 非常精确地规定了浮点数的位布局。

此函数具有基于 Float.Model 的逻辑模型。

从 UInt32 逐位转换。把 UInt32 解释为 Float32，忽略数值，仅将 UInt32 的位模式视为 Float32。

在所有受支持平台上，Float32 与 UInt32 的字节序相同。IEEE 754 非常精确地规定了浮点数的位布局。

此函数具有基于 Float32.Model 的逻辑模型。

把 64 位浮点数转换为 32 位浮点数。 这可能损失精度。

此函数不在内核中规约。

把 32 位浮点数转换为 64 位浮点数。

此函数不在内核中规约。

把浮点数转换为字符串。

此函数不在内核中规约。

把浮点数转换为字符串。

此函数不在内核中规约。

把浮点数转换为8 位无符号整数。

若给定的 Float 非负，则向下舍入，把值截断为正整数，并钳制到 UInt8 的范围。返回 0，当 Float 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt8 值（即 UInt8.size - 1）。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的8 位有符号整数。

若 Float 大于 Int8 的最大值（包括 Inf），则返回 Int8 的最大值（即 Int8.maxValue）。若它小于 Int8 的最小值（包括 -Inf），则返回 Int8 的最小值（即 Int8.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数转换为8 位无符号整数。

若给定的 Float32 非负，则向下舍入，把值截断为正整数，并钳制到 UInt8 的范围。返回 0，当 Float32 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt8 值（即 UInt8.size - 1）。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的8 位有符号整数。

若 Float 大于 Int8 的最大值（包括 Inf），则返回 Int8 的最大值（即 Int8.maxValue）。若它小于 Int8 的最小值（包括 -Inf），则返回 Int8 的最小值（即 Int8.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数转换为16 位无符号整数。

若给定的 Float 非负，则向下舍入，把值截断为正整数，并钳制到 UInt16 的范围。返回 0，当 Float 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt16 值（即 UInt16.size - 1）。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的16 位有符号整数。

若 Float 大于 Int16 的最大值（包括 Inf），则返回 Int16 的最大值（即 Int16.maxValue）。若它小于 Int16 的最小值（包括 -Inf），则返回 Int16 的最小值（即 Int16.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数转换为16 位无符号整数。

若给定的 Float32 非负，则向下舍入，把值截断为正整数，并钳制到 UInt16 的范围。返回 0，当 Float32 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt16 值（即 UInt16.size - 1）。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的16 位有符号整数。

若 Float 大于 Int16 的最大值（包括 Inf），则返回 Int16 的最大值（即 Int16.maxValue）。若它小于 Int16 的最小值（包括 -Inf），则返回 Int16 的最小值（即 Int16.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数转换为32 位无符号整数。

若给定的 Float 非负，则向下舍入，把值截断为正整数，并钳制到 UInt32 的范围。返回 0，当 Float 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt32 值（即 UInt32.size - 1）。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数转换为32 位无符号整数。

若给定的 Float32 非负，则向下舍入，把值截断为正整数，并钳制到 UInt32 的范围。返回 0，当 Float32 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt32 值（即 UInt32.size - 1）。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的32 位有符号整数。

若 Float 大于 Int32 的最大值（包括 Inf），则返回 Int32 的最大值（即 Int32.maxValue）。若它小于 Int32 的最小值（包括 -Inf），则返回 Int32 的最小值（即 Int32.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的32 位有符号整数。

若 Float 大于 Int32 的最大值（包括 Inf），则返回 Int32 的最大值（即 Int32.maxValue）。若它小于 Int32 的最小值（包括 -Inf），则返回 Int32 的最小值（即 Int32.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数转换为64 位无符号整数。

若给定的 Float 非负，则向下舍入，把值截断为正整数，并钳制到 UInt64 的范围。返回 0，当 Float 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt64 值（即 UInt64.size - 1）。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的64 位有符号整数。

若 Float 大于 Int64 的最大值（包括 Inf），则返回 Int64 的最大值（即 Int64.maxValue）。若它小于 Int64 的最小值（包括 -Inf），则返回 Int64 的最小值（即 Int64.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数转换为64 位无符号整数。

若给定的 Float32 非负，则向下舍入，把值截断为正整数，并钳制到 UInt64 的范围。返回 0，当 Float32 为负数或 NaN；若浮点数大于该最大值，则返回最大的 UInt64 值（即 UInt64.size - 1）。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的64 位有符号整数。

若 Float 大于 Int64 的最大值（包括 Inf），则返回 Int64 的最大值（即 Int64.maxValue）。若它小于 Int64 的最小值（包括 -Inf），则返回 Int64 的最小值（即 Int64.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数转换为机器字长无符号整数。

若给定的 Float 非负，则向下舍入，把值截断为正整数，并钳制到 USize 的范围。返回 0，当 Float 为负数或 NaN；若浮点数大于该最大值，则返回最大的 USize 值（即 USize.size - 1）。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数转换为机器字长无符号整数。

若给定的 Float32 非负，则向下舍入，把值截断为正整数，并钳制到 USize 的范围。返回 0，当 Float32 为负数或 NaN；若浮点数大于该最大值，则返回最大的 USize 值（即 USize.size - 1）。

此函数具有基于 Float32.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的机器字长有符号整数。

若 Float 大于 ISize 的最大值（包括 Inf），则返回 ISize 的最大值（即 ISize.maxValue）。若它小于 ISize 的最小值（包括 -Inf），则返回 ISize 的最小值（即 ISize.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float.Model 的逻辑模型。

把浮点数向零舍入，截断为最接近的机器字长有符号整数。

若 Float 大于 ISize 的最大值（包括 Inf），则返回 ISize 的最大值（即 ISize.maxValue）。若它小于 ISize 的最小值（包括 -Inf），则返回 ISize 的最小值（即 ISize.minValue）。若它为 NaN，则返回 0。

此函数具有基于 Float32.Model 的逻辑模型。

把整数转换为最接近的 64 位浮点数；若超出 Float 的范围，则转换为正无穷或负无穷浮点值。

把整数转换为最接近的 32 位浮点数；若超出 Float32 的范围，则转换为正无穷或负无穷浮点值。

把自然数转换为最接近的 64 位浮点数；若超出 Float 的范围，则转换为无穷浮点值。

把自然数转换为最接近的 32 位浮点数；若超出 Float32 的范围，则转换为无穷浮点值。

把给定浮点数 x 拆分为有效数/指数对 (s, i)，满足 x = s * 2^i，其中 s ∈ (-1;-0.5] ∪ [0.5; 1)。若 x 不是有限数，则返回未定义值。

此函数不在内核中规约。编译后代码由 C 函数 frexp 实现。

把给定浮点数 x 拆分为有效数/指数对 (s, i)，满足 x = s * 2^i，其中 s ∈ (-1;-0.5] ∪ [0.5; 1)。若 x 不是有限数，则返回未定义值。

此函数不在内核中规约。编译后代码由 C 函数 frexp 实现。

按照 IEEE 754 检查两个浮点数是否相等。

浮点相等与命题等式并不对应。特别地，由于 NaN != NaN，它不具自反性；又由于 0.0 == -0.0 但 1.0 / 0.0 != 1.0 / -0.0，它也不是同余关系。

此函数不在内核中规约，并被编译为 C 相等运算符。

按照 IEEE 754 检查两个浮点数是否相等。

浮点相等与命题等式并不对应。特别地，由于 NaN != NaN，它不具自反性；又由于 0.0 == -0.0 但 1.0 / 0.0 != 1.0 / -0.0，它也不是同余关系。

此函数不在内核中规约，并被编译为 C 相等运算符。

按照 IEEE 754 将两个 64 位浮点数相加。通常通过 + 运算符使用。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 加法运算符。

按照 IEEE 754 将两个 32 位浮点数相加。通常通过 + 运算符使用。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 加法运算符。

按照 IEEE 754 将两个 64 位浮点数相减。通常通过 - 运算符使用。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 减法运算符。

按照 IEEE 754 将两个 32 位浮点数相减。通常通过 - 运算符使用。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 减法运算符。

按照 IEEE 754 将两个 64 位浮点数相乘。通常通过 * 运算符使用。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 乘法运算符。

按照 IEEE 754 将两个 32 位浮点数相乘。通常通过 * 运算符使用。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 乘法运算符。

按照 IEEE 754 将两个 64 位浮点数相除。通常通过 / 运算符使用。

在 Lean 中，除以零通常得到零；但对 Float 而言，结果会是 Inf、-Inf 或 NaN。

此函数具有基于 Float.Model 的逻辑模型，并被编译为 C 除法运算符。

按照 IEEE 754 将两个 32 位浮点数相除。通常通过 / 运算符使用。

在 Lean 中，除以零通常得到零；但对 Float32 而言，结果会是 Inf、-Inf 或 NaN。

此函数具有基于 Float32.Model 的逻辑模型，并被编译为 C 除法运算符。

把一个浮点数提升到另一个浮点数次幂。通常通过 ^ 运算符使用。

此函数不在内核中规约。编译后代码由 C 函数 pow 实现。

把一个浮点数提升到另一个浮点数次幂。通常通过 ^ 运算符使用。

此函数不在内核中规约。编译后代码由 C 函数 powf 实现。

计算浮点数的指数 e^x。

此函数不在内核中规约。编译后代码由 C 函数 exp 实现。

计算浮点数的指数 e^x。

此函数不在内核中规约。编译后代码由 C 函数 expf 实现。

计算浮点数以 2 为底的指数 2^x。

此函数不在内核中规约。编译后代码由 C 函数 exp2 实现。

计算浮点数以 2 为底的指数 2^x。

此函数不在内核中规约。编译后代码由 C 函数 exp2f 实现。

计算浮点数的自然对数 ln x。

此函数不在内核中规约。编译后代码由 C 函数 log 实现。

计算浮点数的自然对数 ln x。

此函数不在内核中规约。编译后代码由 C 函数 logf 实现。

计算浮点数以 10 为底的对数。

此函数不在内核中规约。编译后代码由 C 函数 log10 实现。

计算浮点数以 10 为底的对数。

此函数不在内核中规约。编译后代码由 C 函数 log10f 实现。

计算浮点数以 2 为底的对数。

此函数不在内核中规约。编译后代码由 C 函数 log2 实现。

计算浮点数以 2 为底的对数。

此函数不在内核中规约。编译后代码由 C 函数 log2f 实现。

高效计算 x * 2^i。

此函数不在内核中规约。

高效计算 x * 2^i。

此函数不在内核中规约。

舍入到最近的整数；恰好位于中点时，向远离零的方向舍入。

此函数不在内核中规约。编译后代码由 C 函数 round 实现。

舍入到最近的整数；恰好位于中点时，向远离零的方向舍入。

此函数不在内核中规约。编译后代码由 C 函数 roundf 实现。

计算浮点数的下取整，即不大于给定数的最大整数。

此函数不在内核中规约。编译后代码由 C 函数 floor 实现。

示例：

• Float.floor 1.5 = 1

• Float.floor (-1.5) = (-2)

计算浮点数的下取整，即不大于给定数的最大整数。

此函数不在内核中规约。编译后代码由 C 函数 floorf 实现。

示例：

• Float32.floor 1.5 = 1

• Float32.floor (-1.5) = (-2)

计算浮点数的上取整，即不小于给定数的最小整数。

此函数不在内核中规约。编译后代码由 C 函数 ceil 实现。

示例：

• Float.ceil 1.5 = 2

• Float.ceil (-1.5) = (-1)

计算浮点数的上取整，即不小于给定数的最小整数。

此函数不在内核中规约。编译后代码由 C 函数 ceilf 实现。

示例：

• Float32.ceil 1.5 = 2

• Float32.ceil (-1.5) = (-1)