summaryrefslogtreecommitdiff
path: root/src/theory/arith/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/kinds')
-rw-r--r--src/theory/arith/kinds15
1 files changed, 12 insertions, 3 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index fd784ccce..f6540b9da 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -1,3 +1,12 @@
-PLUS
-MULT
-UMINUS
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/expr/builtin_kinds.
+#
+
+operator PLUS "arithmetic addition"
+operator MULT "arithmetic multiplication"
+operator UMINUS "arithmetic negation"
+
+constant CONST_RATIONAL ::CVC4::Rational "a multiple-precision rational constant"
+constant CONST_INTEGER ::CVC4::Integer "a multiple-precision integer constant"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback