a choice of two states (flag nonzero: the first)
230def arenaSelectState =
231 (lambda unrestricted flag : Nat .
232 (lambda unrestricted whenNonzero : (family ArenaScheduleState) . (lambda unrestricted whenZero : (family ArenaScheduleState) .
233 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaScheduleState)) whenZero
234 (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family ArenaScheduleState) . whenNonzero)) flag))))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.