628def modelWord64MultiplyStep =
629 (lambda unrestricted state : (family ModelWord64MultiplyState) .
630 (eliminate
631 ModelWord64MultiplyState
632 (lambda unrestricted current : (family ModelWord64MultiplyState) .
633 (family ModelWord64MultiplyState))
634 state
635 (branch
636 ModelWord64MultiplyStateValue
637 multiplicand
638 multiplier
639 product
640 overflow
641 .
642 (app
643 (lambda unrestricted leastBit : Nat .
644 (app
645 (lambda unrestricted nextMultiplier : (family ModelWord64) .
646 (eliminate
647 ModelWord64AddResult
648 (lambda unrestricted result : (family ModelWord64AddResult) .
649 (family ModelWord64MultiplyState))
650 (modelWord64AddWithCarry product multiplicand)
651 (branch
652 ModelWord64AddResultValue
653 sum
654 carry
655 .
656 (constructor
657 ModelWord64MultiplyState
658 ModelWord64MultiplyStateValue
659 (modelWord64ShiftLeftOne multiplicand)
660 nextMultiplier
661 (modelWord64Select leastBit sum product)
662 (modelWord64FlagOr
663 overflow
664 (modelWord64FlagOr
665 (modelWord64FlagAnd leastBit carry)
666 (modelWord64FlagAnd
667 (modelWord64HighBit multiplicand)
668 (modelWord64FlagNot (modelWord64IsZero nextMultiplier)))))))))
669 (modelWord64ShiftRightOne multiplier)))
670 (modelWord64LeastBit multiplier)))))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.