aboutsummaryrefslogtreecommitdiff
path: root/LeanAStarTest.lean
diff options
context:
space:
mode:
Diffstat (limited to 'LeanAStarTest.lean')
-rw-r--r--LeanAStarTest.lean14
1 files changed, 14 insertions, 0 deletions
diff --git a/LeanAStarTest.lean b/LeanAStarTest.lean
new file mode 100644
index 0000000..adca44d
--- /dev/null
+++ b/LeanAStarTest.lean
@@ -0,0 +1,14 @@
+import LeanAStarTest.Tests
+
+def main (params : List String) : IO UInt32 := do
+ if !params.isEmpty then
+ IO.println "Currently LeanAStarTest will run all tests, and not accept parameters."
+ return ⟨UInt32.size-1,by decide⟩
+ let mut result : UInt32 := 0
+ for (testName, test) in LeanAStarTests.ListTests do
+ if let Except.error e := test () then
+ IO.println s!"{testName} failed: {e}"
+ result := result + 1
+ else
+ IO.println s!"{testName} succeeded."
+ return result