Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7795–7817

workReduceCorePayloadUnary

Full file
7795def workReduceCorePayloadUnary =
7796  (lambda unrestricted inspect : (pi unrestricted term : (family CoreTerm) . (pi unrestricted selected : (pi unrestricted payload : Bytes . (family CoreWorkResult)) . (pi unrestricted fallback : (pi unrestricted force : Nat . (family CoreWorkResult)) . (family CoreWorkResult)))) .
7797    (lambda unrestricted primitive : (family CorePrimitive) .
7798      (lambda unrestricted argument : (family CoreTerm) .
7799        (lambda unrestricted budget : (family NormalizationBudget) .
7800          (inspect
7801            argument
7802            (lambda unrestricted payload : Bytes .
7803              (coreWorkChargeBytes
7804                payload
7805                budget
7806                (lambda unrestricted remaining : (family NormalizationBudget) .
7807                  (constructor
7808                    CoreWorkResult
7809                    CoreWorkCompleted
7810                    (reduceDirectCorePrimitive primitive argument)
7811                    remaining))))
7812            (lambda unrestricted force : Nat .
7813              (constructor
7814                CoreWorkResult
7815                CoreWorkCompleted
7816                (corePrimitiveApplication primitive argument)
7817                budget)))))))

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.