Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 12078–12096

coreBindContinuationType

Full file
12078def coreBindContinuationType =
12079  (lambda unrestricted effects : (family CoreTerm) .
12080    (lambda unrestricted resultType : (family CoreTerm) .
12081      (lambda unrestricted inputType : (family CoreTerm) .
12082        (constructor
12083          CoreTerm
12084          CorePi
12085          coreUnrestricted
12086          (constructor
12087            CoreTerm
12088            CorePi
12089            coreUnrestricted
12090            inputType
12091            (coreComputationType
12092              (shiftCoreBy (succ zero) effects)
12093              (shiftCoreBy (succ zero) resultType)))
12094          (coreComputationType
12095            (shiftCoreBy (succ zero) effects)
12096            (shiftCoreBy (succ zero) resultType))))))

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.