Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20

def · lines 1681–1694

deviceArenaCarriedAnywhere

Full file
---- (D) over the executed instances ---- the first instance breaking (D), as `base` + its index; 0 when none does. The build's evaluator evaluates both arms of a choice, so each step makes exactly one recursive call (the walk goes on past a hazard; the first one found wins). every plane some phase carries
1681def deviceArenaCarriedAnywhere =
1682  (lambda unrestricted phases : (family DeviceArenaPhases) .
1683    (eliminate
1684      DeviceArenaPhases
1685      (lambda unrestricted current : (family DeviceArenaPhases) . (family ArenaResidents))
1686      phases
1687      (branch DeviceArenaPhasesEnd . (constructor ArenaResidents ArenaResidentsEnd))
1688      (branch
1689        DeviceArenaPhasesNext
1690        head
1691        tail
1692        induction
1693        .
1694        (deviceArenaAppend (deviceArenaPhaseCarriedOf head) induction))))

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.