Skip to content

Commit aafb96f

Browse files
committed
chore: generalize type of isBlackListed (#7136)
easier to use from, say, `MetaM` or `CommandElabM` this way.
1 parent 1328e6e commit aafb96f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Lean/Expr/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ def isInternal' (declName : Name) : Bool :=
103103
open Meta
104104

105105
-- from Lean.Server.Completion
106-
def isBlackListed (declName : Name) : CoreM Bool := do
106+
def isBlackListed {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
107107
if declName == ``sorryAx then return true
108108
if declName matches .str _ "inj" then return true
109109
if declName matches .str _ "noConfusionType" then return true

0 commit comments

Comments
 (0)