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/kinds4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 508106106..44474c18a 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -302,9 +302,6 @@ operator SEXPR 0: "a symbolic expression (any arity)"
operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body"
-## for co-datatypes, not yet supported
-# operator MU 2 "mu"
-
parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
constant CHAIN_OP \
::CVC4::Chain \
@@ -336,7 +333,6 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
-#typerule MU ::CVC4::theory::builtin::MuTypeRule
typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback