diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-04 19:55:16 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-09 17:21:42 -0400 |
| commit | 42d28850d4f2f4816af24dedf8d1cbd0a0d58b6f (patch) | |
| tree | a1183f01ad74389d5e6c5d9c949e18d25f75d1cd /src/theory | |
| parent | 9d0734cf73454ecfd51556ca84daaba9025b28f8 (diff) | |
Support empty (and 1-ary) tuples and records.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/datatypes/kinds | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 2e58677df..81ef32b32 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -88,7 +88,7 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType # constructor applications are constant if they are applied only to constants construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule -operator TUPLE_TYPE 1: "tuple type" +operator TUPLE_TYPE 0: "tuple type" cardinality TUPLE_TYPE \ "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ "theory/datatypes/theory_datatypes_type_rules.h" @@ -100,7 +100,7 @@ enumerator TUPLE_TYPE \ "::CVC4::theory::datatypes::TupleEnumerator" \ "theory/datatypes/type_enumerator.h" -operator TUPLE 1: "a tuple" +operator TUPLE 0: "a tuple" typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule construle TUPLE ::CVC4::theory::datatypes::TupleProperties |