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 1029–1049

deviceArenaWidenLaunch

Full file
1029def deviceArenaWidenLaunch =
1030  (lambda unrestricted steps : Nat .
1031    (lambda unrestricted launch : (family DeviceArenaLaunch) .
1032      (eliminate
1033        DeviceArenaLaunch
1034        (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch))
1035        launch
1036        (branch
1037          DeviceArenaLaunchValue
1038          identity
1039          base
1040          generators
1041          spans
1042          .
1043          (constructor
1044            DeviceArenaLaunch
1045            DeviceArenaLaunchValue
1046            identity
1047            base
1048            generators
1049            (deviceArenaWiden steps (deviceArenaStands generators) spans))))))

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.