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 12195–12211

inferCorePrimitiveApplication

Full file
12195def inferCorePrimitiveApplication =
12196  (lambda unrestricted argument : (family CoreTerm) .
12197    (lambda unrestricted functionResult : (family CoreInferenceResult) .
12198      (lambda unrestricted argumentResult : (family CoreInferenceResult) .
12199        (lambda unrestricted primitive : (family CorePrimitive) .
12200          (nat-eliminate
12201            (lambda unrestricted special : Nat . (family CoreInferenceResult))
12202            (inferCoreApplicationDefault argument functionResult argumentResult)
12203            (lambda unrestricted predecessor : Nat .
12204              (lambda unrestricted induction : (family CoreInferenceResult) .
12205                (inferCoreEffectHead argument argumentResult)))
12206            (nat-eliminate
12207              (lambda unrestricted returnMatch : Nat . Nat)
12208              (corePrimitiveMatches primitive (constructor CorePrimitive CoreBind))
12209              (lambda unrestricted predecessor : Nat .
12210                (lambda unrestricted induction : Nat . (succ zero)))
12211              (corePrimitiveMatches primitive (constructor CorePrimitive CoreReturn))))))))

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.