338def checkpointManifestFrom =
339 (lambda unrestricted capture : (family CheckpointCapture) .
340 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
341 (eliminate
342 StdList
343 (lambda unrestricted current : (family StdList (family CheckpointLogicalRegion)) .
344 (pi unrestricted ordinal : Nat .
345 (pi unrestricted groups : (family StdList (family CheckpointCapturedRegion)) . Nat)))
346 regions
347 (branch
348 StdListEmpty
349 .
350 (lambda unrestricted ordinal : Nat .
351 (lambda unrestricted groups : (family StdList (family CheckpointCapturedRegion)) .
352 (stdBoolToNatural (stdListIsEmpty (family CheckpointCapturedRegion) groups)))))
353 (branch
354 StdListCons
355 region
356 tail
357 induction
358 .
359 (lambda unrestricted ordinal : Nat .
360 (lambda unrestricted groups : (family StdList (family CheckpointCapturedRegion)) .
361 (eliminate
362 StdList
363 (lambda unrestricted current : (family StdList (family CheckpointCapturedRegion)) .
364 Nat)
365 groups
366 (branch StdListEmpty . 0)
367 (branch
368 StdListCons
369 group
370 after
371 ignored
372 .
373 (naturalAnd
374 (checkpointCapturedRegionValid region ordinal capture group)
375 (induction (succ ordinal) after))))))))))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.