Append once at the outer continuation. Repeated/conditional bodies keep
their original ends; appending there would duplicate the continuation.
447def appendGlobalProtocol =
448 (lambda erased operation : Type 0 .
449 (lambda erased payload : Type 0 .
450 (lambda erased decision : Type 0 .
451 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
452 (lambda unrestricted tail : (family GlobalProtocol operation payload decision) .
453 (eliminate
454 GlobalProtocol
455 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
456 (family GlobalProtocol operation payload decision))
457 program
458 (branch GlobalProtocolEnd . tail)
459 (branch
460 GlobalProtocolLocal
461 role
462 value
463 rest
464 induction
465 .
466 (constructor
467 GlobalProtocol
468 GlobalProtocolLocal
469 operation
470 payload
471 decision
472 role
473 value
474 induction))
475 (branch
476 GlobalProtocolTransfer
477 identity
478 value
479 rest
480 induction
481 .
482 (constructor
483 GlobalProtocol
484 GlobalProtocolTransfer
485 operation
486 payload
487 decision
488 identity
489 value
490 induction))
491 (branch
492 GlobalProtocolRepeat
493 count
494 body
495 rest
496 bodyResult
497 restResult
498 .
499 (constructor
500 GlobalProtocol
501 GlobalProtocolRepeat
502 operation
503 payload
504 decision
505 count
506 body
507 restResult))
508 (branch
509 GlobalProtocolChoice
510 identity
511 selector
512 announcements
513 zeroBody
514 oneBody
515 rest
516 zeroResult
517 oneResult
518 restResult
519 .
520 (constructor
521 GlobalProtocol
522 GlobalProtocolChoice
523 operation
524 payload
525 decision
526 identity
527 selector
528 announcements
529 zeroBody
530 oneBody
531 restResult))))))))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.