addition of two FINITE values: ONE rounding (the strong normalizer normalizes
every branch of a select, so the rounding must sit outside the selects)
149def modelAddFinite =
150 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
151 (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
152 (modelZeroOf (modelAnd (modelSign a) (modelSign b)))
153 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat) (modelSumSigned a b)
154 (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Hundred50))))))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.