The same tree and global protocol, projected for another role (admission
checks both ends of every transfer).
230def nativeCombineForRole =
231 (lambda unrestricted context : (family NativeCombineContext) .
232 (lambda unrestricted role : Nat .
233 (nat-eliminate
234 (lambda unrestricted flag : Nat . (family NativeCombineContext))
235 (let unrestricted projected =
236 (projectGlobalProtocol
237 (family OrderedCombineOperation (family RegionTransferIdentity))
238 (family RegionTransferIdentity)
239 (family ProtocolNoDecision)
240 role
241 (nativeCombineGlobal context))
242 in
243 (constructor
244 NativeCombineContext
245 NativeCombineContextOf
246 role
247 (nativeCombineTree context)
248 (nativeCombineDigest context)
249 (nativeCombineAnchor context)
250 (nativeCombineGlobal context)
251 projected
252 (participantProtocolPayloads
253 (family OrderedCombineOperation (family RegionTransferIdentity))
254 (family RegionTransferIdentity)
255 (family ProtocolNoDecision)
256 projected)))
257 (lambda unrestricted prior : Nat .
258 (lambda unrestricted ignored : (family NativeCombineContext) . context))
259 (naturalEqual role (nativeCombineRole context)))))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.