922def lookupCorePrimitive : (pi unrestricted name : Bytes . (family CorePrimitiveLookupResult)) =
923 (lambda unrestricted name : Bytes .
924 (chooseCorePrimitive
925 (coreBytesEqual name b"byte-equal")
926 (constructor CorePrimitive CoreByteEqual)
927 (chooseCorePrimitive
928 (coreBytesEqual name b"byte-less-than")
929 (constructor CorePrimitive CoreByteLess)
930 (chooseCorePrimitive
931 (coreBytesEqual name b"nat-less-than")
932 (constructor CorePrimitive CoreNaturalLess)
933 (chooseCorePrimitive
934 (coreBytesEqual name b"nat-to-byte")
935 (constructor CorePrimitive CoreNaturalToByte)
936 (chooseCorePrimitive
937 (coreBytesEqual name b"byte-to-nat")
938 (constructor CorePrimitive CoreByteToNatural)
939 (chooseCorePrimitive
940 (coreBytesEqual name b"bytes-append")
941 (constructor CorePrimitive CoreBytesAppend)
942 (chooseCorePrimitive
943 (coreBytesEqual name b"bytes-cons")
944 (constructor CorePrimitive CoreBytesCons)
945 (chooseCorePrimitive
946 (coreBytesEqual name b"bytes-length")
947 (constructor CorePrimitive CoreBytesLength)
948 (chooseCorePrimitive
949 (coreBytesEqual name b"nat-eliminate")
950 (constructor CorePrimitive CoreNaturalEliminate)
951 (chooseCorePrimitive
952 (coreBytesEqual
953 name
954 b"bytes-eliminate")
955 (constructor CorePrimitive CoreBytesEliminate)
956 (chooseCorePrimitive
957 (coreBytesEqual name b"bytes-equal")
958 (constructor CorePrimitive CoreBytesEqual)
959 (lookupCoreIndexedBytesPrimitive name)))))))))))))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.