270def numericalCheckExact =
271 (lambda unrestricted contract : (family NumericalContract) .
272 (eliminate
273 NumericalRelation
274 (lambda unrestricted current : (family NumericalRelation) .
275 (family StdResult (family NumericalFailure) Nat))
276 (numericalRelationOf contract)
277 (branch
278 NumericalExactOrder
279 identity
280 .
281 (numericalRequire
282 Nat
283 (naturalAnd
284 (naturalNonzero (bytes-length identity))
285 (numericalIdentityPresent (stdNumericProfileIdentityOf (numericalProfileOf contract))))
286 (constructor NumericalFailure NumericalEmptyIdentity)
287 (numericalRequire
288 Nat
289 (naturalLess
290 (numericalSubnormalCode (stdNumericProfileSubnormalsOf (numericalProfileOf contract)))
291 2)
292 (constructor NumericalFailure NumericalUnknownSubnormals)
293 (numericalRequire
294 Nat
295 (naturalIsZero
296 (numericalContractionCode
297 (stdNumericProfileContractionOf (numericalProfileOf contract))))
298 (constructor NumericalFailure NumericalUnspecifiedContraction)
299 (numericalCheckOperations
300 (numericalProfileOf contract)
301 (numericalOperationsOf contract))))))
302 (branch
303 NumericalBoundedDifference
304 reference
305 norm
306 tensors
307 tolerance
308 .
309 (constructor
310 StdResult
311 StdFailure
312 (family NumericalFailure)
313 Nat
314 (constructor NumericalFailure NumericalBoundEvidenceRequired)))
315 (branch
316 NumericalApproximateTransition
317 transition
318 schema
319 .
320 (constructor
321 StdResult
322 StdFailure
323 (family NumericalFailure)
324 Nat
325 (constructor NumericalFailure NumericalTransitionEvidenceRequired)))))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.