extending the trivial example

h0nzZik · Apr 15, 2024 · 208128c · 208128c
1 parent 2165767
commit 208128c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/minuska/bin/main.ml b/minuska/bin/main.ml
@@ -7,6 +7,7 @@ let builtins_alist =
   [ "bool.neg", "b_bool_neg";
     "bool.and", "b_and";
     "bool.or", "b_or";
+    "bool.eq", "b_eq";
     "bool.false", "b_false";
     "bool.true", "b_true";
     "term.same_symbol", "b_have_same_symbol";

diff --git a/minuska/trivial.m b/minuska/trivial.m
@@ -4,6 +4,10 @@
 
 strictness: [] ;
 
+rule [stmt.ite.false]:
+	ite[B,X,Y] => Y where bool.eq(B, bool.false())
+    ;
+
 rule [while.unfold]:
 	while[B,X] => ite[B, seq[X, while[B, X]], unitValue[]]
 	where bool.true()