61def magnitudeDecodeCanonical =
62 (lambda unrestricted digits : Bytes .
63 (app
64 (nat-eliminate
65 (lambda unrestricted flag : Nat .
66 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
67 (lambda unrestricted force : Nat .
68 (constructor
69 NaturalMagnitudeResult
70 NaturalMagnitudeRejected
71 (constructor NaturalMagnitudeFailure NaturalMagnitudeNonCanonical)))
72 (lambda unrestricted predecessor : Nat .
73 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
74 (lambda unrestricted force : Nat . (magnitudeBudgetAccept digits))))
75 (Std.Natural/naturalAnd
76 (magnitudeDigitsValid digits)
77 (bytes-equal digits (magnitudeNormalize digits))))
78 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.