503def buildNamedCoreConstructorApplication :
504 (pi unrestricted familyName : Bytes .
505 (pi unrestricted constructorName : Bytes .
506 (pi unrestricted expectedArity : Nat .
507 (pi unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
508 (family NamedCoreApplicationBuildResult))))) =
509 (lambda unrestricted familyName : Bytes .
510 (lambda unrestricted constructorName : Bytes .
511 (lambda unrestricted expectedArity : Nat .
512 (lambda unrestricted arguments : (family ApplicationBuilderNamedCoreArguments) .
513 (nat-eliminate
514 (lambda unrestricted matched : Nat .
515 (family NamedCoreApplicationBuildResult))
516 (constructor NamedCoreApplicationBuildResult NamedCoreApplicationRejected
517 (constructor ApplicationBuilderError
518 ApplicationBuilderConstructorArityMismatch
519 expectedArity
520 (app applicationBuilderNamedCoreArgumentCount arguments))
521 (constructor ApplicationBuilderTelemetry
522 ApplicationBuilderTelemetryValue
523 expectedArity
524 (app applicationBuilderNamedCoreArgumentCount arguments)
525 zero
526 (succ zero)
527 zero
528 zero
529 zero
530 applicationBuilderArityCode))
531 (lambda unrestricted predecessor : Nat .
532 (lambda unrestricted induction : (family NamedCoreApplicationBuildResult) .
533 (constructor NamedCoreApplicationBuildResult NamedCoreApplicationBuilt
534 (constructor NamedCoreTerm NamedCoreConstructorApplication
535 familyName
536 constructorName
537 (app applicationBuilderNamedCoreArgumentSequence arguments))
538 (constructor ApplicationBuilderTelemetry
539 ApplicationBuilderTelemetryValue
540 expectedArity
541 (app applicationBuilderNamedCoreArgumentCount arguments)
542 zero
543 (succ zero)
544 zero
545 zero
546 zero
547 applicationBuilderSuccessCode))))
548 (app
549 (app naturalEqual expectedArity)
550 (app applicationBuilderNamedCoreArgumentCount 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.