AlphaGitHub
Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

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

family · lines 319–325

CoreReductionResult

Full file
A completed result has reached a fixed point; exhaustion retains only a resumable residual and never claims it is a normal form. Counts are rounds, not node visits or wall-clock work.
319family CoreReductionResult : Type 0
320constructor CoreReductionCompleted
321field unrestricted coreReductionFixedPoint : (family CoreTerm)
322field unrestricted coreReductionCompletedRounds : Nat
323constructor CoreReductionExhausted
324field unrestricted coreReductionResidual : (family CoreTerm)
325field unrestricted coreReductionExhaustedRounds : Nat

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.