The reduce-and-deliver global protocol under an admitted numerical
contract, for a caller composing it into a larger round; the delivery
must be the placement context's.
758def planNativeCombineGlobalDelivering =
759 (lambda unrestricted placement : (family NativeCombinePlacement) .
760 (lambda unrestricted delivery : (family CombineDelivery) .
761 (lambda unrestricted required : (family NumericalContract) .
762 (lambda unrestricted participants : Nat .
763 (lambda unrestricted members : (family CombineCoverage) .
764 (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
765 (planNumericalCombineAndDeliver
766 (family RegionTransferIdentity)
767 required
768 required
769 participants
770 members
771 baseAnchor
772 nativeCombineBinding
773 (nativeCombineLocalAdmitted placement)
774 (nativeCombineTransferAdmitted placement)
775 delivery
776 (nativeCombineTree (nativeCombinePlacementContext placement))
777 nativeCombineEnd)))))))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.