457def modelWord64AddChecked =
458 (lambda unrestricted left : (family ModelWord64) .
459 (lambda unrestricted right : (family ModelWord64) .
460 (eliminate
461 ModelWord64AddResult
462 (lambda unrestricted result : (family ModelWord64AddResult) .
463 (family ModelWord64CheckedResult))
464 (modelWord64AddWithCarry left right)
465 (branch
466 ModelWord64AddResultValue
467 value
468 carry
469 .
470 (nat-eliminate
471 (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
472 (constructor ModelWord64CheckedResult ModelWord64CheckedSucceeded value)
473 (lambda unrestricted predecessor : Nat .
474 (lambda unrestricted induction : (family ModelWord64CheckedResult) .
475 (constructor
476 ModelWord64CheckedResult
477 ModelWord64CheckedFailed
478 (constructor ModelWord64ArithmeticErrorCode ModelWord64AdditionOverflow))))
479 carry)))))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.