2428def dpoPublication =
2429 (lambda unrestricted c : Nat .
2430 (lambda unrestricted u : Nat .
2431 (lambda unrestricted system : (family DataParallelSystem c u) .
2432 (lambda unrestricted q : Nat .
2433 (lambda unrestricted p : Nat .
2434 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
2435 (lambda unrestricted star : (family NativeDataParallelOwnedStarLayout) .
2436 (lambda unrestricted resume : Nat .
2437 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
2438 (constructor
2439 NativePeerRegionPublication
2440 NativePeerRegionPublicationOf
2441 (constructor
2442 NativeRegionCheckpoint
2443 NativeRegionCheckpointOf
2444 (nativeRegionManifest (dpoCheckpoint star))
2445 (nativeRegionShards (dpoCheckpoint star))
2446 (naturalAdd (nativeRegionEpoch (dpoCheckpoint star)) resume)
2447 (nativeRegionEnd (dpoCheckpoint star)))
2448 (naturalPredecessor (dpOwners c u system))
2449 (lambda unrestricted owner : Nat .
2450 (niFrameAt
2451 (dpPublicationIdentity c u system (dpoDigest layout) 0 owner 0)
2452 (dpoStateBytes c u system q p)
2453 (dpoCapture star)))
2454 (lambda unrestricted owner : Nat .
2455 (niFrameAt
2456 (dpPublicationIdentity c u system (dpoDigest layout) 1 0 owner)
2457 dpWord
2458 (dpoCommitted star)))
2459 (nativePeerEdgeConnectionTo edges)
2460 (dpoStateAt layout)
2461 (dpoStateBytes c u system q p)
2462 (dpoAgreedBytes c u system q p)
2463 (dpoShardOwner c u system q p)
2464 (dpoShardOffset c u system q p)
2465 (dpoPaths c u system q p)))))))))))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.