summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2023-06-18 19:09:19 +0200
committerSon Ho2023-06-18 19:09:19 +0200
commit04cefd3b4f3d2c11cfc3542a5ad6fae31dae4796 (patch)
tree9d85e842b0bb89a472499680743b2314a5d4922e /backends/lean/Base
parentccc97b46c166a45255096d3fec2444c90f7c5aaa (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--backends/lean/Base.lean1
-rw-r--r--backends/lean/Base/Primitives.lean5
2 files changed, 3 insertions, 3 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 92e87e6c..f6a78bba 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -1,2 +1,3 @@
import Base.Primitives
import Base.Diverge
+import Base.TestTactics
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