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/kinds8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index fca79aff0..6a6fb2e31 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,7 +300,12 @@ operator SEXPR 0: "a symbolic expression"
operator LAMBDA 2 "lambda"
-parameterized CHAIN BUILTIN 2: "chain operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator"
+constant CHAIN_OP \
+ ::CVC4::Chain \
+ ::CVC4::ChainHashFunction \
+ "util/chain.h" \
+ "the chained operator"
constant TYPE_CONSTANT \
::CVC4::TypeConstant \
@@ -344,6 +349,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
+typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
constant SUBTYPE_TYPE \
::CVC4::Predicate \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback