311def checkpointCapturedRegionValid =
312 (lambda unrestricted region : (family CheckpointLogicalRegion) .
313 (lambda unrestricted ordinal : Nat .
314 (lambda unrestricted capture : (family CheckpointCapture) .
315 (lambda unrestricted group : (family CheckpointCapturedRegion) .
316 (let unrestricted shards =
317 (checkpointCapturedShards group)
318 in
319 (naturalAnd
320 (naturalEqual ordinal (checkpointCapturedOrdinal group))
321 (naturalAnd
322 (intervalPartitionValid
323 (logicalCheckpointExtent region)
324 (stdListMap
325 (family CheckpointPreparedShard)
326 (family LogicalInterval)
327 checkpointShardInterval
328 shards))
329 (stdListFold
330 (family CheckpointPreparedShard)
331 Nat
332 (lambda unrestricted shard : (family CheckpointPreparedShard) .
333 (lambda unrestricted rest : Nat .
334 (naturalAnd (checkpointPreparedShardValid region capture shard) rest)))
335 1
336 shards))))))))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.