Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 412–438

coreQuaternaryType

Full file
412def coreQuaternaryType :
413  (pi unrestricted first : (family CoreTerm) .
414    (pi unrestricted second : (family CoreTerm) .
415      (pi unrestricted third : (family CoreTerm) .
416        (pi unrestricted fourth : (family CoreTerm) .
417          (pi unrestricted result : (family CoreTerm) . (family CoreTerm)))))) =
418  (lambda unrestricted first : (family CoreTerm) .
419    (lambda unrestricted second : (family CoreTerm) .
420      (lambda unrestricted third : (family CoreTerm) .
421        (lambda unrestricted fourth : (family CoreTerm) .
422          (lambda unrestricted result : (family CoreTerm) .
423            (constructor
424              CoreTerm
425              CorePi
426              coreUnrestricted
427              first
428              (constructor
429                CoreTerm
430                CorePi
431                coreUnrestricted
432                second
433                (constructor
434                  CoreTerm
435                  CorePi
436                  coreUnrestricted
437                  third
438                  (constructor CoreTerm CorePi coreUnrestricted fourth result)))))))))

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.