Fix bug in reduceLib.NOT_CONV

Thanks to someplaceguy for bug report.
someplaceguy · Sep 9, 2024 · 7bf55e0 · 7bf55e0
1 parent 3f726a4
commit 7bf55e0
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/num/reduce/src/Boolconv.sml b/src/num/reduce/src/Boolconv.sml
@@ -46,7 +46,7 @@ fun NOT_CONV tm =
  let val xn = dest_neg tm
  in if aconv xn T then c1 else
     if aconv xn F then c2
-    else let val xn' = dest_neg xn in SPEC xn c3 end
+    else let val xn' = dest_neg xn in SPEC xn' c3 end
  end handle HOL_ERR _ => raise ERR "NOT_CONV" ""
 end;
 

diff --git a/src/num/reduce/src/selftest.sml b/src/num/reduce/src/selftest.sml
@@ -38,5 +38,10 @@ val _ = app (fn (n,c,t) => convtest(n,c,lhs t,rhs t)) [
   ("EVEN_CONV(3)", EVEN_CONV, “EVEN 0 <=> T”),
   ("ODD_CONV(1)", ODD_CONV, “ODD 106 <=> F”),
   ("ODD_CONV(2)", ODD_CONV, “ODD 103 <=> T”),
-  ("ODD_CONV(3)", ODD_CONV, “ODD 0 <=> F”)
+  ("ODD_CONV(3)", ODD_CONV, “ODD 0 <=> F”),
+
+  ("NOT_CONV(1)", NOT_CONV, “~T <=> F”),
+  ("NOT_CONV(2)", NOT_CONV, “~F <=> T”),
+  ("NOT_CONV(3)", NOT_CONV, “~~p <=> p”),
+  ("NOT_CONV(4)", NOT_CONV, “~~~q <=> ~q”)
 ]