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 409–420

applicationBuilderNamedCoreArgumentSequence

Full file
409def applicationBuilderNamedCoreArgumentSequence :
410  (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
411    (family NamedCoreTerm)) =
412  (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
413    (eliminate ApplicationBuilderNamedCoreArguments
414      (lambda unrestricted value : (family ApplicationBuilderNamedCoreArguments) .
415        (family NamedCoreTerm))
416      arguments
417      (branch ApplicationBuilderNamedCoreArgumentsEnd .
418        (constructor NamedCoreTerm NamedCoreTermSequenceEnd))
419      (branch ApplicationBuilderNamedCoreArgumentsNext argument remaining induction .
420        (constructor NamedCoreTerm NamedCoreTermSequenceNext argument induction))))

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.