Declared transfer storage occurrences, for local allocation/setup. Repeats
contribute their body once; both choice arms remain visible. This does not
report runtime completions or authorize rearming an unselected transfer.
384def participantProtocolPayloads =
385 (lambda erased operation : Type 0 .
386 (lambda erased payload : Type 0 .
387 (lambda erased decision : Type 0 .
388 (lambda unrestricted program : (family ParticipantProtocol operation payload decision) .
389 (eliminate
390 ParticipantProtocol
391 (lambda unrestricted current : (family ParticipantProtocol operation payload decision) .
392 (family StdList payload))
393 program
394 (branch ParticipantProtocolEnd . (constructor StdList StdListEmpty payload))
395 (branch ParticipantProtocolLocal value rest induction . induction)
396 (branch
397 ParticipantProtocolTransfer
398 direction
399 identity
400 value
401 rest
402 induction
403 .
404 (constructor StdList StdListCons payload value induction))
405 (branch
406 ParticipantProtocolRepeat
407 count
408 body
409 rest
410 bodyResult
411 restResult
412 .
413 (stdListAppend payload bodyResult restResult))
414 (branch
415 ParticipantProtocolChoice
416 role
417 identity
418 selector
419 announcements
420 zeroBody
421 oneBody
422 rest
423 zeroResult
424 oneResult
425 restResult
426 .
427 (stdListAppend
428 payload
429 (eliminate
430 ProtocolAnnouncements
431 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
432 (family StdList payload))
433 announcements
434 (branch ProtocolAnnouncementsEnd . (constructor StdList StdListEmpty payload))
435 (branch
436 ProtocolAnnouncementsNext
437 identity
438 value
439 rest
440 induction
441 .
442 (constructor StdList StdListCons payload value induction)))
443 (stdListAppend payload zeroResult (stdListAppend payload oneResult 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.