the intervals of `count` iterations, each the previous moved by `delta`
823def deviceArenaIterations =
824 (lambda unrestricted count : Nat .
825 (lambda unrestricted delta : Nat .
826 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
827 (app
828 (nat-eliminate
829 (lambda unrestricted remaining : Nat .
830 (pi unrestricted current : (family DeviceArenaIntervals) .
831 (family DeviceArenaIntervals)))
832 (lambda unrestricted current : (family DeviceArenaIntervals) .
833 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
834 (lambda unrestricted p : Nat .
835 (lambda unrestricted induction : (pi unrestricted current : (family DeviceArenaIntervals) . (family DeviceArenaIntervals)) .
836 (lambda unrestricted current : (family DeviceArenaIntervals) .
837 (deviceArenaMoved
838 0
839 current
840 (induction
841 (deviceArenaMoved
842 delta
843 current
844 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)))))))
845 count)
846 intervals))))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.