239def magnitudeAdd =
240 (lambda unrestricted left : Bytes .
241 (lambda unrestricted right : Bytes .
242 (bytes-builder-build
243 (app
244 (bytes-eliminate
245 (lambda unrestricted rest : Bytes .
246 (pi unrestricted right : Bytes . (pi unrestricted carry : Nat . BytesBuilder)))
247 (lambda unrestricted right : Bytes .
248 (lambda unrestricted carry : Nat .
249 (bytes-builder-chunk
250 (app
251 (nat-eliminate
252 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
253 (lambda unrestricted force : Nat . right)
254 (lambda unrestricted predecessor : Nat .
255 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
256 (lambda unrestricted force : Nat . (magnitudeSuccessorDigits right))))
257 carry)
258 zero))))
259 (lambda unrestricted head : Byte .
260 (lambda unrestricted tail : Bytes .
261 (lambda unrestricted continue : (pi unrestricted right : Bytes . (pi unrestricted carry : Nat . BytesBuilder)) .
262 (lambda unrestricted right : Bytes .
263 (lambda unrestricted carry : Nat .
264 (app
265 (lambda unrestricted total : Nat .
266 (app
267 (nat-eliminate
268 (lambda unrestricted flag : Nat .
269 (pi unrestricted force : Nat . BytesBuilder))
270 (lambda unrestricted force : Nat .
271 (bytes-builder-append
272 (bytes-builder-chunk
273 (bytes-cons
274 (nat-to-byte
275 (Std.Natural/naturalAdd total (byte-to-nat (byte 246))))
276 b""))
277 (continue (bytes-tail right) (succ zero))))
278 (lambda unrestricted predecessor : Nat .
279 (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
280 (lambda unrestricted force : Nat .
281 (bytes-builder-append
282 (bytes-builder-chunk (bytes-cons (nat-to-byte total) b""))
283 (continue (bytes-tail right) zero)))))
284 (nat-less-than total (byte-to-nat (byte 10))))
285 zero))
286 (Std.Natural/naturalAdd
287 carry
288 (Std.Natural/naturalAdd
289 (byte-to-nat head)
290 (byte-to-nat (bytes-head right))))))))))
291 left)
292 right
293 zero))))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.