The first event that breaks the order, counted from 1 (one past the last
when the end does: a submission never awaited, or a write never
consumed), or 0 when none does.
217def arenaScheduleEnd =
218 (lambda unrestricted count : Nat .
219 (lambda unrestricted state : (family ArenaScheduleState) .
220 (let unrestricted hazard = (arenaStateHazardOf state) in
221 (naturalSelect hazard hazard
222 (naturalSelect (naturalAnd (naturalEqual (arenaStateLastOf state) count) (arenaRangesEmpty (arenaStatePendingOf state)))
223 0 (arenaStateIndexOf state))))))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.