218def receiveRegionTransfer =
219 (lambda unrestricted expected : (family RegionTransferIdentity) .
220 (lambda unrestricted actual : (family RegionTransferIdentity) .
221 (lambda unrestricted expectedBytes : Nat .
222 (lambda unrestricted actualBytes : Nat .
223 (lambda unrestricted phase : (family TransferPhase) .
224 (nat-eliminate
225 (lambda unrestricted flag : Nat .
226 (family StdResult (family TransferFailure) (family TransferPhase)))
227 (constructor
228 StdResult
229 StdFailure
230 (family TransferFailure)
231 (family TransferPhase)
232 (constructor TransferFailure TransferIdentityMismatch))
233 (lambda unrestricted previous : Nat .
234 (lambda unrestricted ignored : (family StdResult (family TransferFailure) (family TransferPhase)) .
235 (nat-eliminate
236 (lambda unrestricted flag : Nat .
237 (family StdResult (family TransferFailure) (family TransferPhase)))
238 (constructor
239 StdResult
240 StdFailure
241 (family TransferFailure)
242 (family TransferPhase)
243 (constructor TransferFailure TransferPayloadSizeMismatch))
244 (lambda unrestricted before : Nat .
245 (lambda unrestricted rest : (family StdResult (family TransferFailure) (family TransferPhase)) .
246 (advanceTransferPhase
247 phase
248 (constructor TransferEvent TransferValidatePayload))))
249 (naturalEqual expectedBytes actualBytes))))
250 (regionTransferIdentityEqual expected actual)))))))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.