733def integerLiteralFinish =
734 (lambda unrestricted kind : (family IntegerLiteralKind) .
735 (lambda unrestricted sign : (family IntegerLiteralSign) .
736 (lambda unrestricted width : (family IntegerLiteralWidth) .
737 (lambda unrestricted folded : (family IntegerLiteralFoldResult) .
738 (eliminate
739 IntegerLiteralFoldResult
740 (lambda unrestricted current : (family IntegerLiteralFoldResult) .
741 (family IntegerLiteralResult))
742 folded
743 (branch
744 IntegerLiteralFoldValue
745 magnitude
746 .
747 (eliminate
748 IntegerLiteralSign
749 (lambda unrestricted current : (family IntegerLiteralSign) .
750 (family IntegerLiteralResult))
751 sign
752 (branch
753 IntegerLiteralPositive
754 .
755 (nat-eliminate
756 (lambda unrestricted current : Nat . (family IntegerLiteralResult))
757 (constructor
758 IntegerLiteralResult
759 IntegerLiteralFailed
760 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange))
761 (lambda unrestricted predecessor : Nat .
762 (lambda unrestricted induction : (family IntegerLiteralResult) .
763 (constructor
764 IntegerLiteralResult
765 IntegerLiteralWord
766 width
767 sign
768 (integerLiteralEncodeWidth width magnitude))))
769 (integerLiteralLessOrEqual
770 magnitude
771 (eliminate
772 IntegerLiteralKind
773 (lambda unrestricted current : (family IntegerLiteralKind) .
774 (family ModelWord64))
775 kind
776 (branch IntegerLiteralUnsigned . (integerLiteralUnsignedBound width))
777 (branch IntegerLiteralSigned . (integerLiteralSignedPositiveBound width))))))
778 (branch
779 IntegerLiteralNegative
780 .
781 (eliminate
782 IntegerLiteralKind
783 (lambda unrestricted current : (family IntegerLiteralKind) .
784 (family IntegerLiteralResult))
785 kind
786 (branch
787 IntegerLiteralUnsigned
788 .
789 (constructor
790 IntegerLiteralResult
791 IntegerLiteralFailed
792 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange)))
793 (branch
794 IntegerLiteralSigned
795 .
796 (nat-eliminate
797 (lambda unrestricted current : Nat . (family IntegerLiteralResult))
798 (constructor
799 IntegerLiteralResult
800 IntegerLiteralFailed
801 (constructor IntegerLiteralFailure IntegerLiteralOutOfRange))
802 (lambda unrestricted predecessor : Nat .
803 (lambda unrestricted induction : (family IntegerLiteralResult) .
804 (constructor
805 IntegerLiteralResult
806 IntegerLiteralWord
807 width
808 sign
809 (integerLiteralEncodeWidth
810 width
811 (stdU64SubtractWrapping integerLiteralZero magnitude)))))
812 (integerLiteralLessOrEqual
813 magnitude
814 (integerLiteralSignedNegativeBound width))))))))
815 (branch
816 IntegerLiteralFoldFailed
817 failure
818 .
819 (constructor IntegerLiteralResult IntegerLiteralFailed failure)))))))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.