689def modelWord64MultiplyChecked =
690 (lambda unrestricted left : (family ModelWord64) .
691 (lambda unrestricted right : (family ModelWord64) .
692 (eliminate
693 ModelWord64MultiplyState
694 (lambda unrestricted current : (family ModelWord64MultiplyState) .
695 (family ModelWord64MultiplyCheckedResult))
696 (modelWord64MultiplyStateRun left right)
697 (branch
698 ModelWord64MultiplyStateValue
699 multiplicand
700 multiplier
701 product
702 overflow
703 .
704 (nat-eliminate
705 (lambda unrestricted current : Nat . (family ModelWord64MultiplyCheckedResult))
706 (constructor ModelWord64MultiplyCheckedResult ModelWord64MultiplySucceeded product)
707 (lambda unrestricted predecessor : Nat .
708 (lambda unrestricted induction : (family ModelWord64MultiplyCheckedResult) .
709 (constructor ModelWord64MultiplyCheckedResult ModelWord64MultiplyOverflow)))
710 overflow)))))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.