729def stdU64ToU32Checked =
730 (lambda unrestricted value : (family ModelWord64) .
731 (eliminate
732 ModelWord64
733 (lambda unrestricted current : (family ModelWord64) . (family StdOption (family ModelWord32)))
734 value
735 (branch
736 ModelWord64Value
737 b0
738 b1
739 b2
740 b3
741 b4
742 b5
743 b6
744 b7
745 .
746 (nat-eliminate
747 (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
748 (constructor StdOption StdNone (family ModelWord32))
749 (lambda unrestricted predecessor : Nat .
750 (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
751 (constructor
752 StdOption
753 StdSome
754 (family ModelWord32)
755 (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))))
756 (stdFlagAnd
757 (byte-equal b4 (byte 0))
758 (stdFlagAnd
759 (byte-equal b5 (byte 0))
760 (stdFlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0)))))))))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.