From bb047b8725766cf4562e159d64458fdef89f167b Mon Sep 17 00:00:00 2001
From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Date: Tue, 10 Mar 2026 21:35:47 +0000
Subject: [PATCH] fix: improve `Name.isMetaprogramming` (#12767)

This PR makes sure that identifiers with `Meta` or `Simproc` in their
name do not show up in library search results.

For example, `Nat.Simproc.eq_add_gt` can currently be suggested by
library search, even though it is an implementation detail.
Additionally, there are various declarations in mathlib in the
`Mathlib.Meta` namespace that we do not want to suggest.
---
 src/Lean/Data/Name.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index ba509852f0..00b39c322f 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -205,7 +205,7 @@ def anyS (n : Name) (f : String → Bool) : Bool :=
 /-- Return true if the name is in a namespace associated to metaprogramming. -/
 def isMetaprogramming (n : Name) : Bool :=
   let components := n.components
-  components.head? == some `Lean || (components.any fun n => n == `Tactic || n == `Linter)
+  components.head?.any (· == `Lean) || (components.any (· matches `Tactic | `Linter | `Simproc | `Meta))
 
 end Name
 end Lean