552def buildCoreConstructorApplication :
553 (pi unrestricted familyName : Bytes .
554 (pi unrestricted constructorName : Bytes .
555 (pi unrestricted expectedArity : Nat .
556 (pi unrestricted arguments : (family ApplicationBuilderCoreArguments) .
557 (family CoreApplicationBuildResult))))) =
558 (lambda unrestricted familyName : Bytes .
559 (lambda unrestricted constructorName : Bytes .
560 (lambda unrestricted expectedArity : Nat .
561 (lambda unrestricted arguments : (family ApplicationBuilderCoreArguments) .
562 (nat-eliminate
563 (lambda unrestricted matched : Nat .
564 (family CoreApplicationBuildResult))
565 (constructor CoreApplicationBuildResult CoreApplicationRejected
566 (constructor ApplicationBuilderError
567 ApplicationBuilderConstructorArityMismatch
568 expectedArity
569 (app applicationBuilderCoreArgumentCount arguments))
570 (constructor ApplicationBuilderTelemetry
571 ApplicationBuilderTelemetryValue
572 expectedArity
573 (app applicationBuilderCoreArgumentCount arguments)
574 zero
575 (succ zero)
576 zero
577 zero
578 zero
579 applicationBuilderArityCode))
580 (lambda unrestricted predecessor : Nat .
581 (lambda unrestricted induction : (family CoreApplicationBuildResult) .
582 (constructor CoreApplicationBuildResult CoreApplicationBuilt
583 (constructor CoreTerm CoreConstructorApplication
584 familyName
585 constructorName
586 (app applicationBuilderCoreArgumentSequence arguments))
587 (constructor ApplicationBuilderTelemetry
588 ApplicationBuilderTelemetryValue
589 expectedArity
590 (app applicationBuilderCoreArgumentCount arguments)
591 zero
592 (succ zero)
593 zero
594 zero
595 zero
596 applicationBuilderSuccessCode))))
597 (app
598 (app naturalEqual expectedArity)
599 (app applicationBuilderCoreArgumentCount 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.