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 199–216

appN

Full file
199def appN :
200  (pi unrestricted function : (family Term) .
201    (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
202      (family Term))) =
203  (lambda unrestricted function : (family Term) .
204    (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
205      (app
206        (eliminate ApplicationBuilderTermArguments
207          (lambda unrestricted value : (family ApplicationBuilderTermArguments) .
208            (pi unrestricted accumulated : (family Term) . (family Term)))
209          arguments
210          (branch ApplicationBuilderTermArgumentsEnd .
211            (lambda unrestricted accumulated : (family Term) . accumulated))
212          (branch ApplicationBuilderTermArgumentsNext argument remaining induction .
213            (lambda unrestricted accumulated : (family Term) .
214              (app induction
215                (constructor Term Application accumulated argument)))))
216        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.