440def coreNaturalEliminateType : (family CoreTerm) =
441 (constructor
442 CoreTerm
443 CorePi
444 coreUnrestricted
445 (constructor
446 CoreTerm
447 CorePi
448 coreUnrestricted
449 (constructor CoreTerm CoreNatural)
450 (constructor CoreTerm CoreUniverse zero))
451 (constructor
452 CoreTerm
453 CorePi
454 coreUnrestricted
455 (constructor
456 CoreTerm
457 CoreApplication
458 (constructor CoreTerm CoreBound zero)
459 (constructor CoreTerm CoreNaturalLiteral b""))
460 (constructor
461 CoreTerm
462 CorePi
463 coreUnrestricted
464 (constructor
465 CoreTerm
466 CorePi
467 coreUnrestricted
468 (constructor CoreTerm CoreNatural)
469 (constructor
470 CoreTerm
471 CorePi
472 coreUnrestricted
473 (constructor
474 CoreTerm
475 CoreApplication
476 (constructor CoreTerm CoreBound (succ (succ zero)))
477 (constructor CoreTerm CoreBound zero))
478 (constructor
479 CoreTerm
480 CoreApplication
481 (constructor CoreTerm CoreBound (succ (succ (succ zero))))
482 (constructor
483 CoreTerm
484 CoreNaturalSuccessor
485 (constructor CoreTerm CoreBound (succ zero))))))
486 (constructor
487 CoreTerm
488 CorePi
489 coreUnrestricted
490 (constructor CoreTerm CoreNatural)
491 (constructor
492 CoreTerm
493 CoreApplication
494 (constructor CoreTerm CoreBound (succ (succ (succ zero))))
495 (constructor CoreTerm CoreBound zero))))))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.