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 274–293

namedCoreAppN

Full file
274def namedCoreAppN :
275  (pi unrestricted function : (family NamedCoreTerm) .
276    (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
277      (family NamedCoreTerm))) =
278  (lambda unrestricted function : (family NamedCoreTerm) .
279    (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
280      (app
281        (eliminate ApplicationBuilderNamedCoreArguments
282          (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) .
283            (pi unrestricted accumulated : (family NamedCoreTerm) .
284              (family NamedCoreTerm)))
285          arguments
286          (branch ApplicationBuilderNamedCoreArgumentsEnd .
287            (lambda unrestricted accumulated : (family NamedCoreTerm) . accumulated))
288          (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
289            (lambda unrestricted accumulated : (family NamedCoreTerm) .
290              (app induction
291                (constructor NamedCoreTerm NamedCoreApplication
292                  accumulated argument)))))
293        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.