From bb755d62454de30294b3a84c3834f90cc467f604 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Aug 2021 21:27:40 -0700
Subject: [PATCH] feat: add `commitIfNoEx`

---
 src/Lean/Util/MonadBacktrack.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/Util/MonadBacktrack.lean b/src/Lean/Util/MonadBacktrack.lean
index d0532d5a83..77b54c8d0f 100644
--- a/src/Lean/Util/MonadBacktrack.lean
+++ b/src/Lean/Util/MonadBacktrack.lean
@@ -37,6 +37,14 @@ export MonadBacktrack (saveState restoreState)
     restoreState s
     throw ex
 
+@[specialize] def commitIfNoEx [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) : m α := do
+  let s ← saveState
+  try
+    x
+  catch ex =>
+    restoreState s
+    throw ex
+
 @[specialize] def withoutModifyingState [Monad m] [MonadFinally m] [MonadBacktrack s m] (x : m α) : m α := do
   let s ← saveState
   try