From 04cefd3b4f3d2c11cfc3542a5ad6fae31dae4796 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 18 Jun 2023 19:09:19 +0200
Subject: Make minor modifications

---
 backends/lean/Base/Primitives.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 6b922143..d6cc0bad 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -20,9 +20,8 @@ def assertImpl : CommandElab := fun (_stx: Syntax) => do
   runTermElabM (fun _ => do
     let r ← evalTerm Bool (mkConst ``Bool) _stx[1]
     if not r then
-      logInfo "Assertion failed for: "
-      logInfo _stx[1]
-      logError "Expression reduced to false"
+      logInfo ("Assertion failed for:\n" ++ _stx[1])
+      throwError ("Expression reduced to false:\n"  ++ _stx[1])
     pure ())
 
 #eval 2 == 2
-- 
cgit v1.2.3