327def numericalCompatibility =
328 (lambda unrestricted required : (family NumericalContract) .
329 (lambda unrestricted realized : (family NumericalContract) .
330 (stdResultBind
331 (family NumericalFailure)
332 Nat
333 Nat
334 (numericalCheckExact required)
335 (lambda unrestricted admitted : Nat .
336 (stdResultBind
337 (family NumericalFailure)
338 Nat
339 Nat
340 (numericalCheckExact realized)
341 (lambda unrestricted realizedAdmitted : Nat .
342 (numericalRequire
343 Nat
344 (bytes-equal
345 (numericalProfileBytes (numericalProfileOf required))
346 (numericalProfileBytes (numericalProfileOf realized)))
347 (constructor NumericalFailure NumericalProfileMismatch)
348 (numericalRequire
349 Nat
350 (naturalAnd
351 (bytes-equal
352 (numericalExactOrderBytes (numericalRelationOf required))
353 (numericalExactOrderBytes (numericalRelationOf realized)))
354 (bytes-equal
355 (numericalOperationBytes (numericalOperationsOf required))
356 (numericalOperationBytes (numericalOperationsOf realized))))
357 (constructor NumericalFailure NumericalOrderMismatch)
358 numericalAccepted))))))))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.