Finite-domain arithmetic has an explicit refusal outcome. This avoids making
cross-host equality depend on unspecified NaN payload/default bits. Input
and output checks remain in the emitted program, including after overflow.
216def nativeFiniteFloat64Binary =
217 (lambda unrestricted error : Bytes .
218 (lambda unrestricted slot : Nat .
219 (lambda unrestricted operation : (family NativePhysicalFloat64Operation) .
220 (lambda unrestricted destination : Nat .
221 (lambda unrestricted left : Nat .
222 (lambda unrestricted right : Nat .
223 (lambda unrestricted tail : (family NativePhysicalCommands) .
224 (nativeFloat64RequireFinite
225 (nativeMemoryLoad left)
226 slot
227 error
228 (nativeFloat64RequireFinite
229 (nativeMemoryLoad right)
230 slot
231 error
232 (nativeFloat64Binary
233 error
234 operation
235 destination
236 left
237 right
238 (nativeFloat64RequireFinite (nativeMemoryLoad destination) slot error tail)))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.