55def numericalRequire =
56 (lambda erased value : Type 0 .
57 (lambda unrestricted condition : Nat .
58 (lambda unrestricted reason : (family NumericalFailure) .
59 (lambda unrestricted next : (family StdResult (family NumericalFailure) value) .
60 (nat-eliminate
61 (lambda unrestricted flag : Nat . (family StdResult (family NumericalFailure) value))
62 (constructor StdResult StdFailure (family NumericalFailure) value reason)
63 (lambda unrestricted prior : Nat .
64 (lambda unrestricted ignored : (family StdResult (family NumericalFailure) value) .
65 next))
66 condition)))))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.