AlphaGitHub
Source/Packages

Compiler.ApplicationBuilder

packages/compiler/src/Compiler/ApplicationBuilder.alpha

767 lines104 declarations33.8 KiBSHA-256 4afcba25576e
Download exact fileView at revisionf5034773ad4bb52133

def · lines 347–364

coreAppN

Full file
347def coreAppN :
348  (pi unrestricted function : (family CoreTerm) .
349    (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
350      (family CoreTerm))) =
351  (lambda unrestricted function : (family CoreTerm) .
352    (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
353      (app
354        (eliminate ApplicationBuilderCoreArguments
355          (lambda unrestricted value : (family ApplicationBuilderCoreArguments) .
356            (pi unrestricted accumulated : (family CoreTerm) . (family CoreTerm)))
357          arguments
358          (branch ApplicationBuilderCoreArgumentsEnd .
359            (lambda unrestricted accumulated : (family CoreTerm) . accumulated))
360          (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
361            (lambda unrestricted accumulated : (family CoreTerm) .
362              (app induction
363                (constructor CoreTerm CoreApplication accumulated argument)))))
364        function)))

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.