From 07957a2ead1f2b640601e0ce20f3d541f576e262 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 5 Mar 2024 22:51:34 +0100
Subject: [PATCH] chore: more informative tests for debugging

---
 Tests.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Tests.lean b/Tests.lean
index 8dfc057..99bfd23 100644
--- a/Tests.lean
+++ b/Tests.lean
@@ -6,13 +6,10 @@ import Lean
 open SubVerso.Examples (loadExamples Example)
 open Lean.FromJson (fromJson?)
 
-def assert (what : String) (cond : Unit -> Bool) : IO Unit := do
-  if !(cond ()) then
-    throw <| .userError what
-
-
 def main : IO UInt32 := do
   IO.println "Checking that the test project generates at least some deserializable JSON"
   let examples ← loadExamples "demo"
-  assert "Examples are non-empty" fun () => !examples.isEmpty
+  if examples.isEmpty then
+    IO.eprintln "No examples found"
+    return 1
   pure 0