43def magnitudeBudgetAccept =
44 (lambda unrestricted digits : Bytes .
45 (app
46 (nat-eliminate
47 (lambda unrestricted flag : Nat .
48 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
49 (lambda unrestricted force : Nat .
50 (constructor NaturalMagnitudeResult NaturalMagnitudeAccepted digits))
51 (lambda unrestricted predecessor : Nat .
52 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
53 (lambda unrestricted force : Nat .
54 (constructor
55 NaturalMagnitudeResult
56 NaturalMagnitudeRejected
57 (constructor NaturalMagnitudeFailure NaturalMagnitudeTooLarge)))))
58 (nat-less-than magnitudeDigitLimit (bytes-length digits)))
59 zero))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.