AlphaGitHub
Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20
Download exact fileView at revisionf5034773ad4bb52133

def · lines 471–485

deviceArenaAppendLaunches

Full file
471def deviceArenaAppendLaunches =
472  (lambda unrestricted left : (family DeviceArenaLaunches) .
473    (lambda unrestricted right : (family DeviceArenaLaunches) .
474      (eliminate
475        DeviceArenaLaunches
476        (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches))
477        left
478        (branch DeviceArenaLaunchesEnd . right)
479        (branch
480          DeviceArenaLaunchesNext
481          head
482          tail
483          induction
484          .
485          (constructor DeviceArenaLaunches DeviceArenaLaunchesNext 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.