Decimal long division: with remainder < divisor, bringing down one digit
makes the next quotient digit at most nine. The bounded digit loop never
iterates a number of times proportional to the dividend's numeric value.
361def magnitudeDivideDigit =
362 (lambda unrestricted divisor : Bytes .
363 (lambda unrestricted dividend : Bytes .
364 (app
365 (nat-eliminate
366 (lambda unrestricted count : Nat .
367 (pi unrestricted state : (sigma unrestricted quotient : Nat . Bytes) .
368 (sigma unrestricted quotient : Nat . Bytes)))
369 (lambda unrestricted state : (sigma unrestricted quotient : Nat . Bytes) . state)
370 (lambda unrestricted predecessor : Nat .
371 (lambda unrestricted continue : (pi unrestricted state : (sigma unrestricted quotient : Nat . Bytes) . (sigma unrestricted quotient : Nat . Bytes)) .
372 (lambda unrestricted state : (sigma unrestricted quotient : Nat . Bytes) .
373 (app
374 (nat-eliminate
375 (lambda unrestricted smaller : Nat .
376 (pi unrestricted force : Nat . (sigma unrestricted quotient : Nat . Bytes)))
377 (lambda unrestricted force : Nat .
378 (continue
379 (pair
380 (sigma unrestricted quotient : Nat . Bytes)
381 (succ (first state))
382 (magnitudeSubtractOrdered (second state) divisor))))
383 (lambda unrestricted unused : Nat .
384 (lambda unrestricted ignored : (pi unrestricted force : Nat . (sigma unrestricted quotient : Nat . Bytes)) .
385 (lambda unrestricted force : Nat . state)))
386 (magnitudeLessCanonical (second state) divisor))
387 zero))))
388 (byte-to-nat (byte 9)))
389 (pair (sigma unrestricted quotient : Nat . Bytes) zero dividend))))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.