--- 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