summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Utils.lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Utils.lean')
-rw-r--r--backends/lean/Base/Utils.lean4
1 files changed, 4 insertions, 0 deletions
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 1f8f1455..5224e1c3 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -301,6 +301,10 @@ example : Nat := by
example (x : Bool) : Nat := by
cases x <;> custom_let x := 3 <;> apply x
+-- Attempt to apply a tactic
+def tryTac (tac : TacticM Unit) : TacticM Unit := do
+ let _ ← tryTactic tac
+
-- Repeatedly apply a tactic
partial def repeatTac (tac : TacticM Unit) : TacticM Unit := do
try