Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 12532–12568

finishInferCoreLetAnnotation

Full file
12532def finishInferCoreLetAnnotation =
12533  (lambda unrestricted annotation : (family CoreTerm) .
12534    (lambda unrestricted value : (family CoreTerm) .
12535      (lambda unrestricted annotationResult : (family CoreInferenceResult) .
12536        (lambda unrestricted valueResult : (family CoreInferenceResult) .
12537          (lambda unrestricted bodyResult : (family CoreInferenceResult) .
12538            (eliminate
12539              CoreInferenceResult
12540              (lambda unrestricted result : (family CoreInferenceResult) .
12541                (family CoreInferenceResult))
12542              annotationResult
12543              (branch
12544                CoreInferred
12545                annotationType
12546                .
12547                (eliminate
12548                  UniverseInspection
12549                  (lambda unrestricted inspection : (family UniverseInspection) .
12550                    (family CoreInferenceResult))
12551                  (inspectUniverse (normalizeCoreType annotationType))
12552                  (branch
12553                    IsUniverse
12554                    level
12555                    .
12556                    (finishInferCoreLetValue annotation value valueResult bodyResult))
12557                  (branch
12558                    NotUniverse
12559                    .
12560                    (constructor
12561                      CoreInferenceResult
12562                      CoreInferenceFailed
12563                      (succ (succ (succ (succ zero))))))))
12564              (branch
12565                CoreInferenceFailed
12566                code
12567                .
12568                (constructor CoreInferenceResult CoreInferenceFailed code))))))))

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.