220def numericalCheckOperations =
221 (lambda unrestricted profile : (family StdNumericProfile) .
222 (lambda unrestricted operations : (family StdList (family StdNumericOperation)) .
223 (eliminate
224 StdList
225 (lambda unrestricted current : (family StdList (family StdNumericOperation)) .
226 (family StdResult (family NumericalFailure) Nat))
227 operations
228 (branch StdListEmpty . numericalAccepted)
229 (branch
230 StdListCons
231 head
232 tail
233 induction
234 .
235 (eliminate
236 StdApproximation
237 (lambda unrestricted current : (family StdApproximation) .
238 (family StdResult (family NumericalFailure) Nat))
239 (stdApproximationOf head (stdNumericProfileTable profile))
240 (branch StdApproximationExact . induction)
241 (branch
242 StdApproximationMaxUlp
243 ulp
244 .
245 (constructor
246 StdResult
247 StdFailure
248 (family NumericalFailure)
249 Nat
250 (constructor NumericalFailure NumericalInexactOperation)))
251 (branch
252 StdApproximationUnmeasured
253 .
254 (constructor
255 StdResult
256 StdFailure
257 (family NumericalFailure)
258 Nat
259 (constructor NumericalFailure NumericalInexactOperation)))
260 (branch
261 StdApproximationUnsupported
262 .
263 (constructor
264 StdResult
265 StdFailure
266 (family NumericalFailure)
267 Nat
268 (constructor NumericalFailure NumericalUnsupportedOperation))))))))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.