every interval moved by `delta` (modulo 2^64), then `rest`
798def deviceArenaMoved =
799 (lambda unrestricted delta : Nat .
800 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
801 (lambda unrestricted rest : (family DeviceArenaIntervals) .
802 (eliminate
803 DeviceArenaIntervals
804 (lambda unrestricted current : (family DeviceArenaIntervals) .
805 (family DeviceArenaIntervals))
806 intervals
807 (branch DeviceArenaIntervalsEnd . rest)
808 (branch
809 DeviceArenaIntervalsNext
810 low
811 high
812 tail
813 induction
814 .
815 (constructor
816 DeviceArenaIntervals
817 DeviceArenaIntervalsNext
818 (deviceArenaAddModulo low delta)
819 (deviceArenaAddModulo high delta)
820 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.