Blob Blame History Raw
--- src/theory/datatypes/kinds.orig	2017-06-23 15:54:52.988063375 -0600
+++ src/theory/datatypes/kinds	2017-07-15 20:30:31.268986539 -0600
@@ -108,4 +108,22 @@ typerule DT_SIZE ::CVC4::theory::datatyp
 operator DT_HEIGHT_BOUND 2 "datatypes height bound"
 typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule
 
+constant TUPLE_SELECT_OP \
+        ::CVC4::TupleSelect \
+        ::CVC4::TupleSelectHashFunction \
+        "util/tuple.h" \
+        "operator for a tuple select"
+
+constant RECORD_OP \
+        ::CVC4::Record \
+        ::CVC4::RecordHashFunction \
+        "expr/record.h" \
+        "operator for a record"
+
+constant RECORD_SELECT_OP \
+        ::CVC4::RecordSelect \
+        ::CVC4::RecordSelectHashFunction \
+        "expr/record.h" \
+        "operator for a record select"
+
 endtheory