add test for reduceBool

leanprover · Oct 11, 2023 · c121aaa · c121aaa
1 parent 9d9b313
commit c121aaa
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 0 deletions.
diff --git a/Lean4Checker.lean b/Lean4Checker.lean
@@ -1,3 +1,4 @@
 import Lean4Checker.Tests.AddFalse
 import Lean4Checker.Tests.AddFalseConstructor
+import Lean4Checker.Tests.ReduceBool
 import Lean4Checker.Tests.UseFalseConstructor
diff --git a/Lean4Checker/Tests/ReduceBool.lean b/Lean4Checker/Tests/ReduceBool.lean
@@ -0,0 +1,7 @@
+def foo : Bool :=
+  match IO.getRandomBytes 1 () with
+  | .ok bs _ => bs[0]! >= 128
+  | _ => false
+theorem T1 : false = Lean.reduceBool foo := rfl
+theorem T2 : Lean.reduceBool foo = true := rfl
+theorem contradiction : False := nomatch T1.trans T2
diff --git a/test.sh b/test.sh
@@ -1,5 +1,9 @@
 #!/bin/bash
 
+# Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
+# we just keep rebuilding until it works!
+until lake build > /dev/null 2>&1; do :; done
+
 check_command() {
     local cmd="$1"
     local expected="$2"
@@ -30,4 +34,6 @@ check_command "lake exe lean4checker Lean4Checker.Tests.AddFalseConstructor" "un
 
 check_command "lake exe lean4checker --fresh Lean4Checker.Tests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
 
+check_command "lake exe lean4checker Lean4Checker.Tests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
+
 echo "All commands produced the expected errors."