Route projection reads the same identity that the wire header encodes;
participant programs must not keep a second, independently chosen route.
254def regionTransferSender =
255 (lambda unrestricted identity : (family RegionTransferIdentity) .
256 (eliminate
257 RegionTransferIdentity
258 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
259 identity
260 (branch
261 RegionTransferIdentityOf
262 composition
263 run
264 region
265 representation
266 round
267 operation
268 sender
269 receiver
270 interval
271 .
272 sender)))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.