Continue only with a completed normal form. Resource exhaustion is distinct
from an inferred type mismatch and never supplies a residual to admission.
11165def withCoreNormalization =
11166 (lambda unrestricted budget : Nat .
11167 (lambda unrestricted term : (family CoreTerm) .
11168 (lambda unrestricted continuation : (pi unrestricted normal : (family CoreTerm) . (family CoreInferenceResult)) .
11169 (eliminate
11170 CoreReductionResult
11171 (lambda unrestricted result : (family CoreReductionResult) . (family CoreInferenceResult))
11172 (normalizeCoreTypeWithBudget budget term)
11173 (branch CoreReductionCompleted normal rounds . (continuation normal))
11174 (branch
11175 CoreReductionExhausted
11176 residual
11177 rounds
11178 .
11179 (constructor
11180 CoreInferenceResult
11181 CoreInferenceFailed
11182 coreNormalizationResourceFailureCode))))))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.