diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
index 1f38cd10e8..83844781fa 100644
--- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
@@ -146,7 +146,7 @@ Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in
 @[inline] def withIncRecDepth (x : SimpM α) : SimpM α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then
+  if max != 0 && curr == max then
     throwMaxRecDepth
   else
     MonadRecDepth.withRecDepth (curr+1) x
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index c1f80b79af..ed7cd6d3bc 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -512,6 +512,15 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
+@[builtin_command_elab «unlock_limits»] def elabUnlockLimits : CommandElab := fun _ => do
+  let opts ← getOptions
+  let opts := maxHeartbeats.set opts 0
+  let opts := maxRecDepth.set opts 0
+  let opts := synthInstance.maxHeartbeats.set opts 0
+  modifyScope ({ · with opts })
+  -- update cached value as well
+  modify ({ · with maxRecDepth := 0 })
+
 open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index a8e107eac5..9747fbf4de 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -245,7 +245,7 @@ We use this combinator to prevent stack overflows.
 @[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then
+  if max != 0 && curr == max then
     throwMaxRecDepthAt (← getRef)
   else
     MonadRecDepth.withRecDepth (curr+1) x
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 9b8d6b4eb3..1a15110689 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -648,6 +648,12 @@ only in a single term or tactic.
 -/
 @[builtin_command_parser] def «set_option»   := leading_parser
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
+/--
+`unlock_limits` disables all built-in resource limit options (currently `maxRecDepth`,
+`maxHeartbeats`, and `synthInstance.maxHeartbeats`) in the current scope by setting them to 0.
+-/
+@[builtin_command_parser] def «unlock_limits» := leading_parser
+  "unlock_limits"
 def eraseAttr := leading_parser
   "-" >> rawIdent
 @[builtin_command_parser] def «attribute»    := leading_parser
diff --git a/src/Lean/Util/RecDepth.lean b/src/Lean/Util/RecDepth.lean
index a44f3c0194..514645bcdf 100644
--- a/src/Lean/Util/RecDepth.lean
+++ b/src/Lean/Util/RecDepth.lean
@@ -14,7 +14,7 @@ namespace Lean
 
 register_builtin_option maxRecDepth : Nat := {
   defValue := defaultMaxRecDepth
-  descr    := "maximum recursion depth for many Lean procedures"
+  descr    := "maximum recursion depth for many Lean procedures, 0 means no limit"
 }
 
 end Lean
diff --git a/tests/elab/unlock_limits.lean b/tests/elab/unlock_limits.lean
new file mode 100644
index 0000000000..eac576f105
--- /dev/null
+++ b/tests/elab/unlock_limits.lean
@@ -0,0 +1,11 @@
+module
+
+import Lean
+
+open Lean in
+unlock_limits in
+run_cmd do
+  let opts ← getOptions
+  assert! maxHeartbeats.get opts == 0
+  assert! maxRecDepth.get opts == 0
+  assert! opts.get? `synthInstance.maxHeartbeats == some (0 : Nat)