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 12484–12500

finishInferCoreLetBody

Full file
12484def finishInferCoreLetBody =
12485  (lambda unrestricted value : (family CoreTerm) .
12486    (lambda unrestricted bodyResult : (family CoreInferenceResult) .
12487      (eliminate
12488        CoreInferenceResult
12489        (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult))
12490        bodyResult
12491        (branch
12492          CoreInferred
12493          bodyType
12494          .
12495          (constructor CoreInferenceResult CoreInferred (substituteCoreTop value bodyType)))
12496        (branch
12497          CoreInferenceFailed
12498          code
12499          .
12500          (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.