the phase of this identity (the first declared; an unknown identity gets
the empty phase, which the caller has refused already)
298def deviceArenaPhaseOf =
299 (lambda unrestricted phases : (family DeviceArenaPhases) .
300 (lambda unrestricted identity : Bytes .
301 (eliminate
302 DeviceArenaPhases
303 (lambda unrestricted current : (family DeviceArenaPhases) . (family DeviceArenaPhase))
304 phases
305 (branch
306 DeviceArenaPhasesEnd
307 .
308 (constructor
309 DeviceArenaPhase
310 DeviceArenaPhaseValue
311 identity
312 (constructor ArenaResidents ArenaResidentsEnd)
313 (constructor ArenaResidents ArenaResidentsEnd)))
314 (branch
315 DeviceArenaPhasesNext
316 head
317 tail
318 induction
319 .
320 (nat-eliminate
321 (lambda unrestricted found : Nat . (family DeviceArenaPhase))
322 induction
323 (lambda unrestricted p : Nat .
324 (lambda unrestricted ignored : (family DeviceArenaPhase) . head))
325 (bytes-equal (deviceArenaPhaseIdentityOf head) identity))))))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.