298def binaryFloatSumSigned =
299 (lambda unrestricted format : (family BinaryFloatFormat) .
300 (lambda unrestricted a : Nat .
301 (lambda unrestricted b : Nat .
302 (modelSelectSigned
303 (specEqual (binaryFloatSign format a) (binaryFloatSign format b))
304 (constructor
305 ModelSigned
306 ModelSignedOf
307 (binaryFloatSign format a)
308 (nat-add (binaryFloatScaledMagnitude format a) (binaryFloatScaledMagnitude format b)))
309 (modelSelectSigned
310 (nat-less-than
311 (binaryFloatScaledMagnitude format a)
312 (binaryFloatScaledMagnitude format b))
313 (constructor
314 ModelSigned
315 ModelSignedOf
316 (binaryFloatSign format b)
317 (nat-subtract
318 (binaryFloatScaledMagnitude format b)
319 (binaryFloatScaledMagnitude format a)))
320 (constructor
321 ModelSigned
322 ModelSignedOf
323 (specSelect
324 (nat-less-than
325 (binaryFloatScaledMagnitude format b)
326 (binaryFloatScaledMagnitude format a))
327 (binaryFloatSign format a)
328 0)
329 (nat-subtract
330 (binaryFloatScaledMagnitude format a)
331 (binaryFloatScaledMagnitude format b))))))))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.