diff options
| author | Son Ho | 2023-06-18 19:09:19 +0200 |
|---|---|---|
| committer | Son Ho | 2023-06-18 19:09:19 +0200 |
| commit | 04cefd3b4f3d2c11cfc3542a5ad6fae31dae4796 (patch) | |
| tree | 9d85e842b0bb89a472499680743b2314a5d4922e /backends/lean/Base | |
| parent | ccc97b46c166a45255096d3fec2444c90f7c5aaa (diff) | |
Make minor modifications
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 |