---- (C) over the launches as written ----
the first launch breaking (C), as 2 + its index among the launches as
written (a repeat's body once); 0 when none does
1377def deviceArenaWordsHazard =
1378 (lambda unrestricted windows : (family ArenaResidents) .
1379 (lambda unrestricted globals : (family ArenaResidents) .
1380 (lambda unrestricted phases : (family DeviceArenaPhases) .
1381 (lambda unrestricted launches : (family DeviceArenaLaunches) .
1382 (app
1383 (eliminate
1384 DeviceArenaLaunches
1385 (lambda unrestricted current : (family DeviceArenaLaunches) .
1386 (pi unrestricted index : Nat . Nat))
1387 launches
1388 (branch DeviceArenaLaunchesEnd . (lambda unrestricted index : Nat . 0))
1389 (branch
1390 DeviceArenaLaunchesNext
1391 head
1392 tail
1393 induction
1394 .
1395 (lambda unrestricted index : Nat .
1396 (let unrestricted identity =
1397 (deviceArenaLaunchIdentityOf head)
1398 in
1399 (let unrestricted later =
1400 (induction (succ index))
1401 in
1402 (nat-eliminate
1403 (lambda unrestricted sound : Nat . Nat)
1404 (naturalAdd 2 index)
1405 (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat . later))
1406 (naturalAnd
1407 (deviceArenaPhaseKnown phases identity)
1408 (deviceArenaSpansNamed
1409 windows
1410 (deviceArenaAppend
1411 (deviceArenaPhasePlanes (deviceArenaPhaseOf phases identity))
1412 globals)
1413 (deviceArenaLaunchSpansOf head)))))))))
1414 0)))))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.