Nonzero n- and m-digit products have at least n+m-1 digits. Refuse
guaranteed overflow before multiplication; the boundary still needs exact admission.
372def magnitudeMultiplyAdmitted =
373 (lambda unrestricted left : Bytes .
374 (lambda unrestricted right : Bytes .
375 (app
376 (nat-eliminate
377 (lambda unrestricted flag : Nat .
378 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
379 (lambda unrestricted force : Nat .
380 (magnitudeAdmitNormalized (magnitudeMultiply left right)))
381 (lambda unrestricted predecessor : Nat .
382 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
383 (lambda unrestricted force : Nat .
384 (constructor
385 NaturalMagnitudeResult
386 NaturalMagnitudeRejected
387 (constructor NaturalMagnitudeFailure NaturalMagnitudeTooLarge)))))
388 (nat-less-than
389 (succ magnitudeDigitLimit)
390 (Std.Natural/naturalAdd (bytes-length left) (bytes-length right))))
391 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.