diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-29 20:27:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-29 20:27:20 -0500 |
commit | 19a93d5e0f924c70e7f77719e0310c730c8fbc61 (patch) | |
tree | 2ce2d68279ebb4b031ab314f7e206862abbc12f8 /src/theory/builtin/kinds | |
parent | b351cce04bc13e00b4b63f1bba403b5d549d56bf (diff) |
Eliminate APPLY kind (#2976)
Diffstat (limited to 'src/theory/builtin/kinds')
-rw-r--r-- | src/theory/builtin/kinds | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 3313a684f..15891dfad 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -289,9 +289,6 @@ constant BUILTIN \ "expr/kind.h" \ "the kind of expressions representing built-in operators" -variable FUNCTION "a defined function" -parameterized APPLY FUNCTION 0: "application of a defined function" - operator EQUAL 2 "equality (two parameters only, sorts must match)" operator DISTINCT 2: "disequality (N-ary, sorts must match)" variable VARIABLE "a variable (not permitted in bindings)" @@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule |