the accumulated deltas applied `steps` times: each span widened to
cover every iteration
854def deviceArenaWiden =
855 (lambda unrestricted steps : Nat .
856 (lambda unrestricted stands : Nat .
857 (lambda unrestricted spans : (family DeviceArenaSpans) .
858 (eliminate
859 DeviceArenaSpans
860 (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans))
861 spans
862 (branch DeviceArenaSpansEnd . (constructor DeviceArenaSpans DeviceArenaSpansEnd))
863 (branch
864 DeviceArenaSpansNext
865 at
866 intervals
867 rise
868 fall
869 uniform
870 last
871 ordinals
872 tail
873 induction
874 .
875 (let unrestricted hull =
876 (constructor
877 DeviceArenaIntervals
878 DeviceArenaIntervalsNext
879 (naturalSaturatingSubtract
880 (deviceArenaLowest intervals)
881 (deviceArenaSaturatingMultiply steps fall))
882 (deviceArenaSaturatingAdd
883 (deviceArenaHighest intervals)
884 (deviceArenaSaturatingMultiply steps rise))
885 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
886 in
887 (let unrestricted exact =
888 (naturalAnd
889 uniform
890 (naturalAnd
891 (naturalEqual (deviceArenaOrdinalsCount ordinals) stands)
892 (naturalLessOrEqual
893 (deviceArenaSaturatingMultiply
894 (succ steps)
895 (deviceArenaIntervalCount intervals))
896 deviceArenaExactIntervals)))
897 in
898 (constructor
899 DeviceArenaSpans
900 DeviceArenaSpansNext
901 at
902 (nat-eliminate
903 (lambda unrestricted adjusted : Nat . (family DeviceArenaIntervals))
904 intervals
905 (lambda unrestricted q : Nat .
906 (lambda unrestricted ignored : (family DeviceArenaIntervals) .
907 (nat-eliminate
908 (lambda unrestricted apart : Nat . (family DeviceArenaIntervals))
909 hull
910 (lambda unrestricted r : Nat .
911 (lambda unrestricted unused : (family DeviceArenaIntervals) .
912 (deviceArenaIterations (succ steps) last intervals)))
913 exact)))
914 (naturalIsZero (deviceArenaOrdinalsEmpty ordinals)))
915 0
916 0
917 1
918 0
919 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)
920 induction))))))))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.