summaryrefslogtreecommitdiff
path: root/src/theory/mktheorytraits
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/mktheorytraits')
-rwxr-xr-xsrc/theory/mktheorytraits7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 983cfade4..15166fc1f 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -345,6 +345,13 @@ function constant {
register_kind "$1" 0 "$5"
}
+function nullaryoperator {
+ # nullaryoperator K ["comment"]
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+ register_kind "$1" 0 "$2"
+}
+
function register_sort {
id=$1
cardinality=$2
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback