add test

runtimeverification · Mar 27, 2024 · 445c36a · 445c36a
1 parent 2995561
commit 445c36a
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/k-distribution/tests/regression-new/macro-rewrite/Makefile b/k-distribution/tests/regression-new/macro-rewrite/Makefile
@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/macro-rewrite/test.k b/k-distribution/tests/regression-new/macro-rewrite/test.k
@@ -0,0 +1,11 @@
+module TEST
+   imports INT
+   imports BOOL
+   imports LIST
+
+   syntax List ::= Int ":" List [macro]
+   rule I : L => ListItem(I) L
+
+   rule (5 => 6) : _
+
+endmodule