456def planNativePeerRegionPublish =
457 (lambda unrestricted publication : (family NativePeerRegionPublication) .
458 (lambda unrestricted available : Nat .
459 (lambda unrestricted role : Nat .
460 (lambda unrestricted success : (family NativePhysicalCommands) .
461 (nat-eliminate
462 (lambda unrestricted valid : Nat .
463 (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)))
464 (constructor
465 StdResult
466 StdFailure
467 (family NativeCheckpointFailure)
468 (family NativePhysicalCommands)
469 (constructor NativeCheckpointFailure NativeCheckpointBounds))
470 (lambda unrestricted previous : Nat .
471 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
472 (constructor
473 StdResult
474 StdSuccess
475 (family NativeCheckpointFailure)
476 (family NativePhysicalCommands)
477 (nativePeerRegionPublish publication role success))))
478 (nativePeerPublicationAdmitted publication available role))))))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.