---- a repeat without its iterations ----
1 when `later` is `earlier` with every awaited and observed generation
`shift` higher, the host's ranges the same: the next iteration of a
repeat body whose generations advance by `shift` an iteration
240def arenaEventShifted =
241 (lambda unrestricted shift : Nat .
242 (lambda unrestricted a : (family ArenaEvent) . (lambda unrestricted b : (family ArenaEvent) .
243 (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) a
244 (branch ArenaHostWrite offset extent .
245 (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
246 (branch ArenaHostWrite o e . (naturalAnd (naturalEqual offset o) (naturalEqual extent e)))
247 (branch ArenaHostRead o e . 0) (branch ArenaAwait g . 0) (branch ArenaObserve g . 0)))
248 (branch ArenaHostRead offset extent .
249 (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
250 (branch ArenaHostWrite o e . 0)
251 (branch ArenaHostRead o e . (naturalAnd (naturalEqual offset o) (naturalEqual extent e)))
252 (branch ArenaAwait g . 0) (branch ArenaObserve g . 0)))
253 (branch ArenaAwait generation .
254 (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
255 (branch ArenaHostWrite o e . 0) (branch ArenaHostRead o e . 0)
256 (branch ArenaAwait g . (naturalEqual g (naturalAdd generation shift))) (branch ArenaObserve g . 0)))
257 (branch ArenaObserve generation .
258 (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) b
259 (branch ArenaHostWrite o e . 0) (branch ArenaHostRead o e . 0) (branch ArenaAwait g . 0)
260 (branch ArenaObserve g . (naturalEqual g (naturalAdd generation shift)))))))))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.