319def modelWord64AddWithCarry =
320 (lambda unrestricted left : (family ModelWord64) .
321 (lambda unrestricted right : (family ModelWord64) .
322 (eliminate
323 ModelWord64
324 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64AddResult))
325 left
326 (branch
327 ModelWord64Value
328 l0
329 l1
330 l2
331 l3
332 l4
333 l5
334 l6
335 l7
336 .
337 (eliminate
338 ModelWord64
339 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64AddResult))
340 right
341 (branch
342 ModelWord64Value
343 r0
344 r1
345 r2
346 r3
347 r4
348 r5
349 r6
350 r7
351 .
352 (eliminate
353 ByteAddResult
354 (lambda unrestricted current : (family ByteAddResult) .
355 (family ModelWord64AddResult))
356 (byteAddWithCarry l0 r0 zero)
357 (branch
358 ByteAddResultValue
359 s0
360 c0
361 .
362 (eliminate
363 ByteAddResult
364 (lambda unrestricted current : (family ByteAddResult) .
365 (family ModelWord64AddResult))
366 (byteAddWithCarry l1 r1 c0)
367 (branch
368 ByteAddResultValue
369 s1
370 c1
371 .
372 (eliminate
373 ByteAddResult
374 (lambda unrestricted current : (family ByteAddResult) .
375 (family ModelWord64AddResult))
376 (byteAddWithCarry l2 r2 c1)
377 (branch
378 ByteAddResultValue
379 s2
380 c2
381 .
382 (eliminate
383 ByteAddResult
384 (lambda unrestricted current : (family ByteAddResult) .
385 (family ModelWord64AddResult))
386 (byteAddWithCarry l3 r3 c2)
387 (branch
388 ByteAddResultValue
389 s3
390 c3
391 .
392 (eliminate
393 ByteAddResult
394 (lambda unrestricted current : (family ByteAddResult) .
395 (family ModelWord64AddResult))
396 (byteAddWithCarry l4 r4 c3)
397 (branch
398 ByteAddResultValue
399 s4
400 c4
401 .
402 (eliminate
403 ByteAddResult
404 (lambda unrestricted current : (family ByteAddResult) .
405 (family ModelWord64AddResult))
406 (byteAddWithCarry l5 r5 c4)
407 (branch
408 ByteAddResultValue
409 s5
410 c5
411 .
412 (eliminate
413 ByteAddResult
414 (lambda unrestricted current : (family ByteAddResult) .
415 (family ModelWord64AddResult))
416 (byteAddWithCarry l6 r6 c5)
417 (branch
418 ByteAddResultValue
419 s6
420 c6
421 .
422 (eliminate
423 ByteAddResult
424 (lambda unrestricted current : (family ByteAddResult) .
425 (family ModelWord64AddResult))
426 (byteAddWithCarry l7 r7 c6)
427 (branch
428 ByteAddResultValue
429 s7
430 c7
431 .
432 (constructor
433 ModelWord64AddResult
434 ModelWord64AddResultValue
435 (constructor
436 ModelWord64
437 ModelWord64Value
438 s0
439 s1
440 s2
441 s3
442 s4
443 s5
444 s6
445 s7)
446 c7)))))))))))))))))))))))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.