From 4b69193442fada85d013f1eef62bd43de0578d90 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 May 2021 18:58:06 -0700
Subject: [PATCH] feat: generalize `withPPInaccessibleNames`

---
 src/Lean/Meta/PPGoal.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 4b22f4c6a2..4615e50841 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -20,9 +20,12 @@ register_builtin_option pp.inaccessibleNames : Bool := {
   descr    := "display inaccessible declarations in the local context"
 }
 
-def withPPInaccessibleNames (x : MetaM α) (flag := true) : MetaM α :=
+def withPPInaccessibleNamesImp (flag : Bool) (x : MetaM α) : MetaM α :=
   withTheReader Core.Context (fun ctx => { ctx with options := pp.inaccessibleNames.setIfNotSet ctx.options flag }) x
 
+def withPPInaccessibleNames [MonadControlT MetaM m] [Monad m] (x : m α) (flag := true) : m α :=
+  mapMetaM (withPPInaccessibleNamesImp flag) x
+
 namespace ToHide
 
 structure State where