each launch moved `shift` ordinals on (a later part of a sequence)
488def deviceArenaShift =
489 (lambda unrestricted shift : Nat .
490 (lambda unrestricted launches : (family DeviceArenaLaunches) .
491 (eliminate
492 DeviceArenaLaunches
493 (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches))
494 launches
495 (branch DeviceArenaLaunchesEnd . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd))
496 (branch
497 DeviceArenaLaunchesNext
498 head
499 tail
500 induction
501 .
502 (constructor
503 DeviceArenaLaunches
504 DeviceArenaLaunchesNext
505 (eliminate
506 DeviceArenaLaunch
507 (lambda unrestricted current : (family DeviceArenaLaunch) .
508 (family DeviceArenaLaunch))
509 head
510 (branch
511 DeviceArenaLaunchValue
512 identity
513 base
514 generators
515 spans
516 .
517 (constructor
518 DeviceArenaLaunch
519 DeviceArenaLaunchValue
520 identity
521 (naturalAdd base shift)
522 generators
523 spans)))
524 induction)))))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.