Source/Packages

Compiler.ApplicationBuilder

packages/compiler/src/Compiler/ApplicationBuilder.alpha

767 lines104 declarations33.8 KiBSHA-256 4afcba25576e

def · lines 386–394

applicationBuilderCoreArgumentCount

Full file
386def applicationBuilderCoreArgumentCount :
387  (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) . Nat) =
388  (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
389    (eliminate ApplicationBuilderCoreArguments
390      (lambda unrestricted value : (family ApplicationBuilderCoreArguments) . Nat)
391      arguments
392      (branch ApplicationBuilderCoreArgumentsEnd . zero)
393      (branch ApplicationBuilderCoreArgumentsNext argument remaining induction .
394        (succ 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.