454def buildTermConstructorApplication :
455 (pi unrestricted familyName : Bytes .
456 (pi unrestricted constructorName : Bytes .
457 (pi unrestricted expectedArity : Nat .
458 (pi unrestricted arguments : (family ApplicationBuilderTermArguments) .
459 (family TermApplicationBuildResult))))) =
460 (lambda unrestricted familyName : Bytes .
461 (lambda unrestricted constructorName : Bytes .
462 (lambda unrestricted expectedArity : Nat .
463 (lambda unrestricted arguments : (family ApplicationBuilderTermArguments) .
464 (nat-eliminate
465 (lambda unrestricted matched : Nat .
466 (family TermApplicationBuildResult))
467 (constructor TermApplicationBuildResult TermApplicationRejected
468 (constructor ApplicationBuilderError
469 ApplicationBuilderConstructorArityMismatch
470 expectedArity
471 (app applicationBuilderTermArgumentCount arguments))
472 (constructor ApplicationBuilderTelemetry
473 ApplicationBuilderTelemetryValue
474 expectedArity
475 (app applicationBuilderTermArgumentCount arguments)
476 zero
477 (succ zero)
478 zero
479 zero
480 zero
481 applicationBuilderArityCode))
482 (lambda unrestricted predecessor : Nat .
483 (lambda unrestricted induction : (family TermApplicationBuildResult) .
484 (constructor TermApplicationBuildResult TermApplicationBuilt
485 (constructor Term ConstructorApplication
486 familyName
487 constructorName
488 (app applicationBuilderTermArgumentSequence arguments))
489 (constructor ApplicationBuilderTelemetry
490 ApplicationBuilderTelemetryValue
491 expectedArity
492 (app applicationBuilderTermArgumentCount arguments)
493 zero
494 (succ zero)
495 zero
496 zero
497 zero
498 applicationBuilderSuccessCode))))
499 (app
500 (app naturalEqual expectedArity)
501 (app applicationBuilderTermArgumentCount arguments)))))))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.