---- the order the launches run ----
the runs of a schedule, from ordinal 0: a repeat's body runs once per
iteration, and neighbouring runs of one phase merge
1428def deviceArenaPrependRun =
1429 (lambda unrestricted identity : Bytes .
1430 (lambda unrestricted first : Nat .
1431 (lambda unrestricted count : Nat .
1432 (lambda unrestricted rest : (family DeviceArenaRuns) .
1433 (eliminate
1434 DeviceArenaRuns
1435 (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaRuns))
1436 rest
1437 (branch
1438 DeviceArenaRunsEnd
1439 .
1440 (constructor DeviceArenaRuns DeviceArenaRunsNext identity first count rest))
1441 (branch
1442 DeviceArenaRunsNext
1443 nextIdentity
1444 nextFirst
1445 nextCount
1446 nextTail
1447 ignored
1448 .
1449 (nat-eliminate
1450 (lambda unrestricted merges : Nat . (family DeviceArenaRuns))
1451 (constructor DeviceArenaRuns DeviceArenaRunsNext identity first count rest)
1452 (lambda unrestricted q : Nat .
1453 (lambda unrestricted unused : (family DeviceArenaRuns) .
1454 (constructor
1455 DeviceArenaRuns
1456 DeviceArenaRunsNext
1457 identity
1458 first
1459 (naturalAdd count nextCount)
1460 nextTail)))
1461 (naturalAnd
1462 (bytes-equal identity nextIdentity)
1463 (naturalEqual (naturalAdd first count) nextFirst)))))))))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.