Source/Packages

Compiler.ApplicationBuilder

packages/compiler/src/Compiler/ApplicationBuilder.alpha

767 lines104 declarations33.8 KiBSHA-256 4afcba25576e

def · lines 396–407

applicationBuilderTermArgumentSequence

Full file
396def applicationBuilderTermArgumentSequence :
397  (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
398    (family Term)) =
399  (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
400    (eliminate ApplicationBuilderTermArguments
401      (lambda unrestricted value : (family ApplicationBuilderTermArguments) .
402        (family Term))
403      arguments
404      (branch ApplicationBuilderTermArgumentsEnd .
405        (constructor Term TermSequenceEnd))
406      (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
407        (constructor Term TermSequenceNext 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.