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 6637–6650

corePrimitiveApplication3

Full file
6637def corePrimitiveApplication3 :
6638  (pi unrestricted primitive : (family CorePrimitive) .
6639    (pi unrestricted first : (family CoreTerm) .
6640      (pi unrestricted second : (family CoreTerm) .
6641        (pi unrestricted third : (family CoreTerm) . (family CoreTerm))))) =
6642  (lambda unrestricted primitive : (family CorePrimitive) .
6643    (lambda unrestricted first : (family CoreTerm) .
6644      (lambda unrestricted second : (family CoreTerm) .
6645        (lambda unrestricted third : (family CoreTerm) .
6646          (constructor
6647            CoreTerm
6648            CoreApplication
6649            (corePrimitiveApplication2 primitive first second)
6650            third)))))

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.