diff --git a/src/Init/Lean/Meta/LevelDefEq.lean b/src/Init/Lean/Meta/LevelDefEq.lean
index 6374137577..2ef2b38d71 100644
--- a/src/Init/Lean/Meta/LevelDefEq.lean
+++ b/src/Init/Lean/Meta/LevelDefEq.lean
@@ -163,6 +163,22 @@ do s ← get;
        (do restore env mctx postponed; pure false))
      (fun ex => do restore env mctx postponed; throw ex)
 
+@[specialize] def tryOpt {α} (x : MetaM (Option α)) : MetaM (Option α) :=
+do s ← get;
+   let env       := s.env;
+   let mctx      := s.mctx;
+   let postponed := s.postponed;
+   modify $ fun s => { postponed := {}, .. s };
+   catch
+     (do a? ← x;
+         match a? with
+         | some a =>
+           condM processPostponed
+             (pure (some a))
+             (do restore env mctx postponed; pure none)
+         | none   => do restore env mctx postponed; pure none)
+     (fun ex => do restore env mctx postponed; throw ex)
+
 /- Public interface -/
 
 def isLevelDefEq (u v : Level) : MetaM Bool :=