781def stdI32ToI8Checked =
782 (lambda unrestricted value : (family StdI32) .
783 (eliminate
784 ModelWord32
785 (lambda unrestricted current : (family ModelWord32) . (family StdOption (family StdI8)))
786 (stdI32ToWord value)
787 (branch
788 ModelWord32Value
789 b0
790 b1
791 b2
792 b3
793 .
794 (app
795 (lambda unrestricted sign : Byte .
796 (nat-eliminate
797 (lambda unrestricted current : Nat . (family StdOption (family StdI8)))
798 (constructor StdOption StdNone (family StdI8))
799 (lambda unrestricted predecessor : Nat .
800 (lambda unrestricted induction : (family StdOption (family StdI8)) .
801 (constructor StdOption StdSome (family StdI8) (stdI8FromByte b0))))
802 (stdFlagAnd
803 (byte-equal b1 sign)
804 (stdFlagAnd (byte-equal b2 sign) (byte-equal b3 sign)))))
805 (stdI8SignByte (stdI8FromByte b0))))))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.