569def modelWord64ShiftLeftOne =
570 (lambda unrestricted value : (family ModelWord64) .
571 (eliminate
572 ModelWord64
573 (lambda unrestricted current : (family ModelWord64) . (family ModelWord64))
574 value
575 (branch
576 ModelWord64Value
577 b0
578 b1
579 b2
580 b3
581 b4
582 b5
583 b6
584 b7
585 .
586 (constructor
587 ModelWord64
588 ModelWord64Value
589 (byteShiftLeftTruncated b0 modelWord64NaturalOne)
590 (byteOr
591 (byteShiftLeftTruncated b1 modelWord64NaturalOne)
592 (byteShiftRight b0 modelWord64NaturalSeven))
593 (byteOr
594 (byteShiftLeftTruncated b2 modelWord64NaturalOne)
595 (byteShiftRight b1 modelWord64NaturalSeven))
596 (byteOr
597 (byteShiftLeftTruncated b3 modelWord64NaturalOne)
598 (byteShiftRight b2 modelWord64NaturalSeven))
599 (byteOr
600 (byteShiftLeftTruncated b4 modelWord64NaturalOne)
601 (byteShiftRight b3 modelWord64NaturalSeven))
602 (byteOr
603 (byteShiftLeftTruncated b5 modelWord64NaturalOne)
604 (byteShiftRight b4 modelWord64NaturalSeven))
605 (byteOr
606 (byteShiftLeftTruncated b6 modelWord64NaturalOne)
607 (byteShiftRight b5 modelWord64NaturalSeven))
608 (byteOr
609 (byteShiftLeftTruncated b7 modelWord64NaturalOne)
610 (byteShiftRight b6 modelWord64NaturalSeven))))))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.