807def stdI32ToI16Checked =
808 (lambda unrestricted value : (family StdI32) .
809 (eliminate
810 ModelWord32
811 (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdI16)))
812 (stdI32ToWord value)
813 (branch
814 ModelWord32Value
815 b0
816 b1
817 b2
818 b3
819 .
820 (app
821 (lambda unrestricted sign : Byte .
822 (nat-eliminate
823 (lambda unrestricted current : Nat . (family StdOption (family StdI16)))
824 (constructor StdOption StdNone (family StdI16))
825 (lambda unrestricted predecessor : Nat .
826 (lambda unrestricted induction : (family StdOption (family StdI16)) .
827 (constructor
828 StdOption
829 StdSome
830 (family StdI16)
831 (stdI16FromU16 (stdU16FromBytes b0 b1)))))
832 (stdFlagAnd (byte-equal b2 sign) (byte-equal b3 sign))))
833 (stdI8SignByte (stdI8FromByte b1))))))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.