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 12425–12442

coreArithmeticAdmissible

Full file
12425def coreArithmeticAdmissible =
12426  (lambda unrestricted operation : (family CoreNaturalOperation) .
12427    (lambda unrestricted left : (family CoreTerm) .
12428      (lambda unrestricted right : (family CoreTerm) .
12429        (eliminate
12430          CoreReductionResult
12431          (lambda unrestricted result : (family CoreReductionResult) . Nat)
12432          (normalizeCoreTypeWithBudget coreNormalizationDefaultRounds left)
12433          (branch
12434            CoreReductionCompleted
12435            normalLeft
12436            rounds
12437            .
12438            (coreArithmeticAdmissionRight
12439              operation
12440              normalLeft
12441              (normalizeCoreTypeWithBudget coreNormalizationDefaultRounds right)))
12442          (branch CoreReductionExhausted residual rounds . zero)))))

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.