142def modelSumSignedValues =
143 (lambda unrestricted a : (family ModelSigned) .
144 (lambda unrestricted b : (family ModelSigned) .
145 (eliminate
146 ModelSigned
147 (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
148 a
149 (branch
150 ModelSignedOf
151 signA
152 magnitudeA
153 .
154 (eliminate
155 ModelSigned
156 (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
157 b
158 (branch
159 ModelSignedOf
160 signB
161 magnitudeB
162 .
163 (modelSelectSigned
164 (specEqual signA signB)
165 (constructor ModelSigned ModelSignedOf signA (nat-add magnitudeA magnitudeB))
166 (modelSelectSigned
167 (nat-less-than magnitudeA magnitudeB)
168 (constructor ModelSigned ModelSignedOf signB (nat-subtract magnitudeB magnitudeA))
169 (constructor
170 ModelSigned
171 ModelSignedOf
172 (specSelect (nat-less-than magnitudeB magnitudeA) signA 0)
173 (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.