614def stdI16ToI32 =
615 (lambda unrestricted value : (family StdI16) .
616 (eliminate
617 StdU16
618 (lambda unrestricted current : (family StdU16) . (family StdI32))
619 (stdI16ToU16 value)
620 (branch
621 StdU16Of
622 low
623 high
624 .
625 (stdI32FromWord
626 (constructor
627 ModelWord32
628 ModelWord32Value
629 low
630 high
631 (nat-eliminate
632 (lambda unrestricted current : Nat . Byte)
633 (byte 255)
634 (lambda unrestricted predecessor : Nat .
635 (lambda unrestricted induction : Byte . (byte 0)))
636 (byte-less-than high (byte 128)))
637 (nat-eliminate
638 (lambda unrestricted current : Nat . Byte)
639 (byte 255)
640 (lambda unrestricted predecessor : Nat .
641 (lambda unrestricted induction : Byte . (byte 0)))
642 (byte-less-than high (byte 128))))))))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.