U8 divides through the core naturals (values are at most 255, so this is
exact on every lane); Std.Natural owns the natural division and its
NaturalDivisionState already carries BOTH the quotient and the remainder, so
one traversal answers both. RECORDED (L11r): the owner's separate
naturalModuloUnchecked is pathological on the reference evaluator (255 mod 16
gives no answer in 100 s while naturalDivideUnchecked 255 16 answers in
0.3 s), which is why the remainder is projected from the state, never
recomputed through the modulo.
1466def stdU8DivRem =
1467 (lambda unrestricted dividend : Byte .
1468 (lambda unrestricted divisor : Byte .
1469 (nat-eliminate
1470 (lambda unrestricted current : Nat . (family StdDivision Byte))
1471 (constructor
1472 StdDivision
1473 StdDivisionFailed
1474 Byte
1475 (constructor StdDivisionErrorCode StdDivisionByZero))
1476 (lambda unrestricted predecessor : Nat .
1477 (lambda unrestricted induction : (family StdDivision Byte) .
1478 (eliminate
1479 NaturalDivisionState
1480 (lambda unrestricted current : (family NaturalDivisionState) .
1481 (family StdDivision Byte))
1482 (naturalDivisionState (byte-to-nat dividend) (byte-to-nat divisor))
1483 (branch
1484 NaturalDivisionStateValue
1485 remainder
1486 quotient
1487 .
1488 (constructor
1489 StdDivision
1490 StdDivisionSucceeded
1491 Byte
1492 (nat-to-byte quotient)
1493 (nat-to-byte remainder))))))
1494 (byte-to-nat divisor))))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.