Compiler.DependentCore

593def corePrimitiveType : (pi unrestricted primitive : (family CorePrimitive) . (family CoreTerm)) =
594  (lambda unrestricted primitive : (family CorePrimitive) .
595    (eliminate
596      CorePrimitive
597      (lambda unrestricted value : (family CorePrimitive) . (family CoreTerm))
598      primitive
599      (branch
600        CoreByteEqual
601        .
602        (coreBinaryType
603          (constructor CoreTerm CoreByte)
604          (constructor CoreTerm CoreByte)
605          (constructor CoreTerm CoreNatural)))
606      (branch
607        CoreByteLess
608        .
609        (coreBinaryType
610          (constructor CoreTerm CoreByte)
611          (constructor CoreTerm CoreByte)
612          (constructor CoreTerm CoreNatural)))
613      (branch
614        CoreNaturalLess
615        .
616        (coreBinaryType
617          (constructor CoreTerm CoreNatural)
618          (constructor CoreTerm CoreNatural)
619          (constructor CoreTerm CoreNatural)))
620      (branch
621        CoreNaturalToByte
622        .
623        (coreUnaryType (constructor CoreTerm CoreNatural) (constructor CoreTerm CoreByte)))
624      (branch
625        CoreByteToNatural
626        .
627        (coreUnaryType (constructor CoreTerm CoreByte) (constructor CoreTerm CoreNatural)))
628      (branch
629        CoreBytesAppend
630        .
631        (coreBinaryType
632          (constructor CoreTerm CoreBytes)
633          (constructor CoreTerm CoreBytes)
634          (constructor CoreTerm CoreBytes)))
635      (branch
636        CoreBytesCons
637        .
638        (coreBinaryType
639          (constructor CoreTerm CoreByte)
640          (constructor CoreTerm CoreBytes)
641          (constructor CoreTerm CoreBytes)))
642      (branch
643        CoreBytesLength
644        .
645        (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreNatural)))
646      (branch CoreNaturalEliminate . coreNaturalEliminateType)
647      (branch CoreBytesEliminate . coreBytesEliminateType)
648      (branch
649        CoreBytesEqual
650        .
651        (coreBinaryType
652          (constructor CoreTerm CoreBytes)
653          (constructor CoreTerm CoreBytes)
654          (constructor CoreTerm CoreNatural)))
655      (branch CoreFileEffect . (constructor CoreTerm CoreUniverse zero))
656      (branch
657        CoreEffects
658        .
659        (coreUnaryType
660          (constructor CoreTerm CoreUniverse zero)
661          (constructor CoreTerm CoreUniverse zero)))
662      (branch
663        CoreComputation
664        .
665        (coreBinaryType
666          (constructor CoreTerm CoreUniverse zero)
667          (constructor CoreTerm CoreUniverse zero)
668          (constructor CoreTerm CoreUniverse zero)))
669      (branch CoreReturn . (constructor CoreTerm CoreUniverse zero))
670      (branch CoreBind . (constructor CoreTerm CoreUniverse zero))
671      (branch
672        CoreReadFile
673        .
674        (coreUnaryType
675          (constructor CoreTerm CoreBytes)
676          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes))))
677      (branch
678        CoreWriteFile
679        .
680        (coreBinaryType
681          (constructor CoreTerm CoreBytes)
682          (constructor CoreTerm CoreBytes)
683          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreNatural))))
684      (branch
685        CoreLinuxOpenNode
686        .
687        (coreUnaryType
688          (constructor CoreTerm CoreBytes)
689          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes))))
690      (branch
691        CoreLinuxCloseNode
692        .
693        (coreUnaryType
694          (constructor CoreTerm CoreBytes)
695          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreNatural))))
696      (branch
697        CoreLinuxIoctl
698        .
699        (coreTernaryType
700          (constructor CoreTerm CoreBytes)
701          (constructor CoreTerm CoreBytes)
702          (constructor CoreTerm CoreBytes)
703          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes))))
704      (branch
705        CoreLinuxMmap
706        .
707        (coreUnaryType
708          (constructor CoreTerm CoreBytes)
709          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreBytes))))
710      (branch
711        CoreLinuxMunmap
712        .
713        (coreBinaryType
714          (constructor CoreTerm CoreBytes)
715          (constructor CoreTerm CoreBytes)
716          (coreComputationType coreFileEffectRow (constructor CoreTerm CoreNatural))))
717      (branch
718        CoreBytesSetIndex
719        .
720        (coreBinaryType
721          (constructor CoreTerm CoreBytes)
722          (constructor CoreTerm CoreNatural)
723          (constructor CoreTerm CoreBytes)))
724      (branch
725        CoreBytesIndexNonzero
726        .
727        (coreBinaryType
728          (constructor CoreTerm CoreBytes)
729          (constructor CoreTerm CoreNatural)
730          (constructor CoreTerm CoreNatural)))
731      (branch
732        CoreBytesSetFreeIndex
733        .
734        (coreQuaternaryType
735          (constructor CoreTerm CoreBytes)
736          (constructor CoreTerm CoreNatural)
737          (constructor CoreTerm CoreNatural)
738          (constructor CoreTerm CoreNatural)
739          (constructor CoreTerm CoreBytes)))
740      (branch CoreBytesBuilderType . (constructor CoreTerm CoreUniverse zero))
741      (branch CoreBytesBuilderEmpty . coreBytesBuilderTerm)
742      (branch
743        CoreBytesBuilderChunk
744        .
745        (coreUnaryType (constructor CoreTerm CoreBytes) coreBytesBuilderTerm))
746      (branch
747        CoreBytesBuilderAppend
748        .
749        (coreBinaryType coreBytesBuilderTerm coreBytesBuilderTerm coreBytesBuilderTerm))
750      (branch
751        CoreBytesBuilderBuild
752        .
753        (coreUnaryType coreBytesBuilderTerm (constructor CoreTerm CoreBytes)))
754      (branch
755        CoreRuntimeImageV4Build
756        .
757        (coreUnaryType coreBytesBuilderTerm (constructor CoreTerm CoreBytes)))
758      (branch
759        CoreBytesHead
760        .
761        (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreByte)))
762      (branch
763        CoreBytesTail
764        .
765        (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes)))
766      (branch
767        CoreBytesChecksum
768        .
769        (coreUnaryType (constructor CoreTerm CoreBytes) (constructor CoreTerm CoreBytes)))))