Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7159–7174

corePrimitiveApplication4

Full file
7159def corePrimitiveApplication4 :
7160  (pi unrestricted primitive : (family CorePrimitive) .
7161    (pi unrestricted first : (family CoreTerm) .
7162      (pi unrestricted second : (family CoreTerm) .
7163        (pi unrestricted third : (family CoreTerm) .
7164          (pi unrestricted fourth : (family CoreTerm) . (family CoreTerm)))))) =
7165  (lambda unrestricted primitive : (family CorePrimitive) .
7166    (lambda unrestricted first : (family CoreTerm) .
7167      (lambda unrestricted second : (family CoreTerm) .
7168        (lambda unrestricted third : (family CoreTerm) .
7169          (lambda unrestricted fourth : (family CoreTerm) .
7170            (constructor
7171              CoreTerm
7172              CoreApplication
7173              (corePrimitiveApplication3 primitive first second third)
7174              fourth))))))

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.