Same total convention as the compile-time core: x/0 = 0, x mod 0 = x.
Inputs use the canonical internal representation; the checked owner admits
external digits before entering this arithmetic layer.
426def magnitudeDivMod =
427 (lambda unrestricted dividend : Bytes .
428 (lambda unrestricted divisor : Bytes .
429 (app
430 (nat-eliminate
431 (lambda unrestricted isZero : Nat .
432 (pi unrestricted force : Nat . (sigma unrestricted quotient : Bytes . Bytes)))
433 (lambda unrestricted force : Nat . (magnitudeDivModNonzero dividend divisor))
434 (lambda unrestricted predecessor : Nat .
435 (lambda unrestricted induction : (pi unrestricted force : Nat . (sigma unrestricted quotient : Bytes . Bytes)) .
436 (lambda unrestricted force : Nat .
437 (pair (sigma unrestricted quotient : Bytes . Bytes) b"" dividend))))
438 (bytes-equal divisor b""))
439 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.