835def stdI64ToI32Checked =
836 (lambda unrestricted value : (family StdI64) .
837 (eliminate
838 ModelWord64
839 (lambda unrestricted current : (family ModelWord64) . (family StdOption (family StdI32)))
840 (stdI64ToWord value)
841 (branch
842 ModelWord64Value
843 b0
844 b1
845 b2
846 b3
847 b4
848 b5
849 b6
850 b7
851 .
852 (app
853 (lambda unrestricted sign : Byte .
854 (nat-eliminate
855 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
856 (constructor StdOption StdNone (family StdI32))
857 (lambda unrestricted predecessor : Nat .
858 (lambda unrestricted induction : (family StdOption (family StdI32)) .
859 (constructor
860 StdOption
861 StdSome
862 (family StdI32)
863 (stdI32FromWord (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3)))))
864 (stdFlagAnd
865 (byte-equal b4 sign)
866 (stdFlagAnd
867 (byte-equal b5 sign)
868 (stdFlagAnd (byte-equal b6 sign) (byte-equal b7 sign))))))
869 (stdI8SignByte (stdI8FromByte b3))))))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.