229def modelFusedFinite =
230 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
231 (specSelect (modelAnd (modelOr (modelIsZero a) (modelIsZero b)) (modelIsZero c))
232 (modelZeroOf (modelAnd (modelXor (modelSign a) (modelSign b)) (modelSign c)))
233 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat)
234 (modelSumSignedValues
235 (constructor ModelSigned ModelSignedOf (modelXor (modelSign a) (modelSign b))
236 (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b)))
237 (modelSignedScale
238 (constructor ModelSigned ModelSignedOf (modelSign c) (modelScaledMagnitude c))
239 modelPow2Hundred50))
240 (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Three00)))))))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.