439def planParticipantProtocol =
440 (lambda erased operation : Type 0 .
441 (lambda erased payload : Type 0 .
442 (lambda erased decision : Type 0 .
443 (lambda unrestricted participants : Nat .
444 (lambda unrestricted participant : Nat .
445 (lambda unrestricted local : (pi unrestricted owner : Nat . (pi unrestricted value : operation . Nat)) .
446 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
447 (lambda unrestricted choice : (pi unrestricted owner : Nat . (pi unrestricted selector : decision . (pi unrestricted announcements : (family ProtocolAnnouncements payload) . Nat))) .
448 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
449 (eliminate
450 StdResult
451 (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
452 (family
453 StdResult
454 (family ProtocolFailure)
455 (family ParticipantProtocol operation payload decision)))
456 (protocolRequire
457 (naturalLess participant participants)
458 (constructor ProtocolFailure ProtocolParticipantBounds)
459 (checkGlobalProtocol
460 operation
461 payload
462 decision
463 participants
464 local
465 transfer
466 choice
467 program))
468 (branch
469 StdFailure
470 error
471 .
472 (constructor
473 StdResult
474 StdFailure
475 (family ProtocolFailure)
476 (family ParticipantProtocol operation payload decision)
477 error))
478 (branch
479 StdSuccess
480 accepted
481 .
482 (constructor
483 StdResult
484 StdSuccess
485 (family ProtocolFailure)
486 (family ParticipantProtocol operation payload decision)
487 (projectGlobalProtocol operation payload decision participant program)))))))))))))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.