428def dpPartitions =
429 (lambda unrestricted c : Nat .
430 (lambda unrestricted u : Nat .
431 (lambda unrestricted system : (family DataParallelSystem c u) .
432 (constructor
433 StdList
434 StdListCons
435 (family CheckpointRegionPartition)
436 (constructor
437 CheckpointRegionPartition
438 CheckpointRegionPartitionOf
439 0
440 (constructor
441 StdList
442 StdListCons
443 (family LogicalInterval)
444 (constructor LogicalInterval LogicalIntervalOf 0 (dpParameterBytes c u system))
445 (constructor StdList StdListEmpty (family LogicalInterval))))
446 (nat-eliminate
447 (lambda unrestricted words : Nat . (family StdList (family CheckpointRegionPartition)))
448 (constructor StdList StdListEmpty (family CheckpointRegionPartition))
449 (lambda unrestricted previous : Nat .
450 (lambda unrestricted ignored : (family StdList (family CheckpointRegionPartition)) .
451 (constructor
452 StdList
453 StdListCons
454 (family CheckpointRegionPartition)
455 (constructor
456 CheckpointRegionPartition
457 CheckpointRegionPartitionOf
458 1
459 (constructor
460 StdList
461 StdListCons
462 (family LogicalInterval)
463 (constructor
464 LogicalInterval
465 LogicalIntervalOf
466 0
467 (dpOptimizerBytes c u system))
468 (constructor StdList StdListEmpty (family LogicalInterval))))
469 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))
470 (dpM c u system))))))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.