summaryrefslogtreecommitdiff
path: root/src/expr/mkmetakind
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/mkmetakind')
-rwxr-xr-xsrc/expr/mkmetakind12
1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 46a69dee5..d84691e14 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -93,6 +93,18 @@ function endtheory {
seen_endtheory=true
}
+function typechecker {
+ # typechecker header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
+function typerule {
+ # typerule OPERATOR typechecking-class
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function rewriter {
# rewriter class header
lineno=${BASH_LINENO[0]}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback