AlphaGitHub
Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796
Download exact fileView at revisionf5034773ad4bb52133

def · lines 5998–6011

workShiftCore

Full file
A zero shift preserves the existing immutable graph. It does not copy the replacement or traverse its descendants merely to return an equal term.
5998def workShiftCore =
5999  (lambda unrestricted term : (family CoreTerm) .
6000    (lambda unrestricted cutoff : Nat .
6001      (lambda unrestricted amount : Nat .
6002        (lambda unrestricted budget : (family NormalizationBudget) .
6003          (coreWorkChoose
6004            (naturalEqual amount zero)
6005            (lambda unrestricted force : Nat .
6006              (coreWorkCharge
6007                coreWorkOne
6008                budget
6009                (lambda unrestricted remaining : (family NormalizationBudget) .
6010                  (constructor CoreWorkResult CoreWorkCompleted term remaining))))
6011            (lambda unrestricted force : Nat . (workShiftCoreTree term cutoff amount 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.