diff options
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d3b9d12fb..47ee8cbfc 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -112,8 +112,14 @@ theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ - "expr/kind.h" "The kind of nodes representing built-in operators" +constant BUILTIN \ + ::CVC4::Kind \ + ::CVC4::kind::KindHashStrategy \ + "expr/kind.h" \ + "The kind of nodes representing built-in operators" + +variable FUNCTION "function" +parameterized APPLY FUNCTION 1: "defined function application" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" |