diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base.lean | 1 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 5 |
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 |