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 1466–1483

deviceArenaRunsShifted

Full file
`runs` moved `shift` on, then `rest`
1466def deviceArenaRunsShifted =
1467  (lambda unrestricted shift : Nat .
1468    (lambda unrestricted runs : (family DeviceArenaRuns) .
1469      (lambda unrestricted rest : (family DeviceArenaRuns) .
1470        (eliminate
1471          DeviceArenaRuns
1472          (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaRuns))
1473          runs
1474          (branch DeviceArenaRunsEnd . rest)
1475          (branch
1476            DeviceArenaRunsNext
1477            identity
1478            first
1479            count
1480            tail
1481            induction
1482            .
1483            (deviceArenaPrependRun identity (naturalAdd first shift) count 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.