From 772beeeb29d5fb2d49e4ecefe30e1d9f26478014 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Sep 2022 22:02:56 -0700
Subject: [PATCH] feat: add `withAtLeastMaxRecDepth`

---
 src/Lean/CoreM.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 1125340456..cbe37fd70f 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -235,6 +235,9 @@ end Core
 
 export Core (CoreM mkFreshUserName checkMaxHeartbeats withCurrHeartbeats)
 
+@[inline] def withAtLeastMaxRecDepth [MonadFunctorT CoreM m] (max : Nat) : m α → m α :=
+  monadMap (m := CoreM) <| withReader (fun ctx => { ctx with maxRecDepth := Nat.max max ctx.maxRecDepth })
+
 @[inline] def catchInternalId [Monad m] [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exception → m α) : m α := do
   try
     x