summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Utils.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Utils.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index e58198f4..5224e1c3 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -303,7 +303,7 @@ example (x : Bool) : Nat := by
-- Attempt to apply a tactic
def tryTac (tac : TacticM Unit) : TacticM Unit := do
- let _ := tryTactic tac
+ let _ ← tryTactic tac
-- Repeatedly apply a tactic
partial def repeatTac (tac : TacticM Unit) : TacticM Unit := do