Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 12027–12076

inferCoreBindResultType

Full file
12027def inferCoreBindResultType =
12028  (lambda unrestricted functionResult : (family CoreInferenceResult) .
12029    (lambda unrestricted resultTypeResult : (family CoreInferenceResult) .
12030      (eliminate
12031        CoreInferenceResult
12032        (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult))
12033        functionResult
12034        (branch
12035          CoreInferred
12036          marker
12037          .
12038          (eliminate
12039            CoreInferenceResult
12040            (lambda unrestricted result : (family CoreInferenceResult) .
12041              (family CoreInferenceResult))
12042            resultTypeResult
12043            (branch
12044              CoreInferred
12045              resultUniverse
12046              .
12047              (eliminate
12048                UniverseInspection
12049                (lambda unrestricted inspection : (family UniverseInspection) .
12050                  (family CoreInferenceResult))
12051                (inspectUniverse resultUniverse)
12052                (branch
12053                  IsUniverse
12054                  level
12055                  .
12056                  (constructor
12057                    CoreInferenceResult
12058                    CoreInferred
12059                    (constructor CoreTerm CoreUniverse zero)))
12060                (branch
12061                  NotUniverse
12062                  .
12063                  (constructor
12064                    CoreInferenceResult
12065                    CoreInferenceFailed
12066                    (succ (succ (succ (succ (succ (succ zero))))))))))
12067            (branch
12068              CoreInferenceFailed
12069              code
12070              .
12071              (constructor CoreInferenceResult CoreInferenceFailed code))))
12072        (branch
12073          CoreInferenceFailed
12074          code
12075          .
12076          (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.