215def modelSumSignedValues =
216 (lambda unrestricted a : (family ModelSigned) . (lambda unrestricted b : (family ModelSigned) .
217 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) a
218 (branch ModelSignedOf signA magnitudeA .
219 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) b
220 (branch ModelSignedOf signB magnitudeB .
221 (modelSelectSigned (specEqual signA signB)
222 (constructor ModelSigned ModelSignedOf signA (nat-add magnitudeA magnitudeB))
223 (modelSelectSigned (nat-less-than magnitudeA magnitudeB)
224 (constructor ModelSigned ModelSignedOf signB (nat-subtract magnitudeB magnitudeA))
225 (constructor ModelSigned ModelSignedOf
226 (specSelect (nat-less-than magnitudeB magnitudeA) signA 0)
227 (nat-subtract magnitudeA magnitudeB))))))))))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.