diff options
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 15891dfad..c90419def 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -300,13 +300,6 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body" -parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction 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 \ - ::CVC4::ChainHashFunction \ - "expr/chain.h" \ - "the chained operator; payload is an instance of the CVC4::Chain class" - constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashFunction \ @@ -334,8 +327,6 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule -typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule -typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule # lambda expressions that are isomorphic to array constants can be considered constants construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule |