1017def checkpointPeerArtifact =
1018 (lambda unrestricted worker : Nat .
1019 (lambda unrestricted port : Nat .
1020 (lambda unrestricted resume : Nat .
1021 (lambda unrestricted steps : Nat .
1022 (nat-eliminate
1023 (lambda unrestricted fits : Nat . Bytes)
1024 b""
1025 (lambda unrestricted previous : Nat .
1026 (lambda unrestricted ignored : Bytes .
1027 (peerLayouts
1028 (lambda unrestricted initial : (family RegionFrameLayout) .
1029 (lambda unrestricted contribution : (family RegionFrameLayout) .
1030 (lambda unrestricted updated : (family RegionFrameLayout) .
1031 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
1032 (lambda unrestricted work : Nat .
1033 (peerCheckpointWithLayouts
1034 worker
1035 port
1036 resume
1037 steps
1038 initial
1039 contribution
1040 updated
1041 acknowledged
1042 work)))))))))
1043 (naturalLessOrEqual steps regionFrameWordLimit))))))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.