487def coppeliusAdamWLaunches =
488 (lambda unrestricted k : Nat .
489 (stdListReverse Nat
490 (nat-eliminate
491 (lambda unrestricted current : Nat . (family StdList Nat))
492 (constructor StdList StdListEmpty Nat)
493 (lambda unrestricted piece : Nat .
494 (lambda unrestricted rest : (family StdList Nat) .
495 (constructor StdList StdListCons Nat (coppeliusAdamWLaunch k piece) rest)))
496 coppeliusAdamWPieces)))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.