summaryrefslogtreecommitdiff
path: root/src/theory/builtin/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/builtin/kinds')
-rw-r--r--src/theory/builtin/kinds3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index c1edd81cb..a04c12903 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -321,6 +321,9 @@ cardinality FUNCTION_TYPE \
"::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
well-founded FUNCTION_TYPE false
+enumerator FUNCTION_TYPE \
+ ::CVC4::theory::builtin::FunctionEnumerator \
+ "theory/builtin/type_enumerator.h"
operator SEXPR_TYPE 0: "the type of a symbolic expression"
cardinality SEXPR_TYPE \
"::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback