497def coreBytesEliminateType : (family CoreTerm) =
498 (constructor
499 CoreTerm
500 CorePi
501 coreUnrestricted
502 (constructor
503 CoreTerm
504 CorePi
505 coreUnrestricted
506 (constructor CoreTerm CoreBytes)
507 (constructor CoreTerm CoreUniverse zero))
508 (constructor
509 CoreTerm
510 CorePi
511 coreUnrestricted
512 (constructor
513 CoreTerm
514 CoreApplication
515 (constructor CoreTerm CoreBound zero)
516 (constructor CoreTerm CoreBytesLiteral b""))
517 (constructor
518 CoreTerm
519 CorePi
520 coreUnrestricted
521 (constructor
522 CoreTerm
523 CorePi
524 coreUnrestricted
525 (constructor CoreTerm CoreByte)
526 (constructor
527 CoreTerm
528 CorePi
529 coreUnrestricted
530 (constructor CoreTerm CoreBytes)
531 (constructor
532 CoreTerm
533 CorePi
534 coreUnrestricted
535 (constructor
536 CoreTerm
537 CoreApplication
538 (constructor CoreTerm CoreBound (succ (succ (succ zero))))
539 (constructor CoreTerm CoreBound zero))
540 (constructor
541 CoreTerm
542 CoreApplication
543 (constructor CoreTerm CoreBound (succ (succ (succ (succ zero)))))
544 (constructor
545 CoreTerm
546 CoreApplication
547 (constructor
548 CoreTerm
549 CoreApplication
550 (constructor
551 CoreTerm
552 CorePrimitiveTerm
553 (constructor CorePrimitive CoreBytesCons))
554 (constructor CoreTerm CoreBound (succ (succ zero))))
555 (constructor CoreTerm CoreBound (succ zero)))))))
556 (constructor
557 CoreTerm
558 CorePi
559 coreUnrestricted
560 (constructor CoreTerm CoreBytes)
561 (constructor
562 CoreTerm
563 CoreApplication
564 (constructor CoreTerm CoreBound (succ (succ (succ zero))))
565 (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.