Std.Word

DIVISION (L11r, NUM-004): see the StdDivision family for the contract. EVALUATOR NOTE (measured at L11r): the reference evaluator is a NORMALIZER -- it normalizes every closed subterm, including the branch an eliminator does not select (a slow closed term under an unselected successor lambda still costs its full time). No shape below therefore makes a REFUSED word division cheap on the evaluator lane: the loop is normalized anyway. The refusal is kept in the zero case and the work under the successor lambda because that is the natural shape (the flag reads "may divide"), not for laziness; the evaluator-lane laws cover U8 (bounded naturals) and the native lane carries every word-width value and refusal (NUM-006).

1132def stdDivisionErrorCodeBytes =
1133  (lambda unrestricted code : (family StdDivisionErrorCode) .
1134    (eliminate
1135      StdDivisionErrorCode
1136      (lambda unrestricted current : (family StdDivisionErrorCode) . Bytes)
1137      code
1138      (branch StdDivisionByZero . b"ALPHA-STD-WORD-001")
1139      (branch StdDivisionOverflow . b"ALPHA-STD-WORD-002")))