From 75db964b0c56f1a3b04b77c33d226c4d9cd0ca54 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Apr 2017 16:47:12 -0500
Subject: Add nullary operator metakind.

---
 src/expr/mkexpr | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/expr/mkexpr')

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 963e297b4..60ee758d8 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -248,6 +248,12 @@ template <> $2 const & Expr::getConst() const {
   case $1: return to->mkConst(n.getConst< $2 >());"
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function check_theory_seen {
   if $seen_endtheory; then
     echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
-- 
cgit v1.2.3