the natural a word holds (its bytes little-endian); below 2^64, so it is
a word of the build's naturals too
757def modelWord64Natural =
758 (lambda unrestricted value : (family ModelWord64) .
759 (eliminate
760 ModelWord64
761 (lambda unrestricted current : (family ModelWord64) . Nat)
762 value
763 (branch
764 ModelWord64Value
765 b0
766 b1
767 b2
768 b3
769 b4
770 b5
771 b6
772 b7
773 .
774 (naturalAdd
775 (byte-to-nat b0)
776 (naturalMultiply
777 256
778 (naturalAdd
779 (byte-to-nat b1)
780 (naturalMultiply
781 256
782 (naturalAdd
783 (byte-to-nat b2)
784 (naturalMultiply
785 256
786 (naturalAdd
787 (byte-to-nat b3)
788 (naturalMultiply
789 256
790 (naturalAdd
791 (byte-to-nat b4)
792 (naturalMultiply
793 256
794 (naturalAdd
795 (byte-to-nat b5)
796 (naturalMultiply
797 256
798 (naturalAdd (byte-to-nat b6) (naturalMultiply 256 (byte-to-nat b7))))))))))))))))))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.