how many ordinals a launch stands for
1013def deviceArenaStands =
1014 (lambda unrestricted generators : (family DeviceArenaGenerators) .
1015 (eliminate
1016 DeviceArenaGenerators
1017 (lambda unrestricted current : (family DeviceArenaGenerators) . Nat)
1018 generators
1019 (branch DeviceArenaGeneratorsEnd . 1)
1020 (branch
1021 DeviceArenaGeneratorsNext
1022 stride
1023 count
1024 tail
1025 induction
1026 .
1027 (naturalMultiply count 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.