oops

src/Lean/LibrarySuggestions/Basic.lean

@@ -300,7 +300,7 @@ def isDeniedPremise (env : Environment) (name : Name) : Bool := Id.run do
   if name == ``sorryAx then return true
   if name.isInternalDetail then return true
   if Lean.Meta.isInstanceCore env name then return true
-  if Lean.Linter.isDeprecated env name then return false
+  if Lean.Linter.isDeprecated env name then return true
   if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
   if let some moduleIdx := env.getModuleIdxFor? name then
     let moduleName := env.header.moduleNames[moduleIdx.toNat]!

tests/lean/run/library_suggestions_deprecated.lean

@@ -0,0 +1,26 @@
+import Lean.LibrarySuggestions.Basic
+
+-- Define a normal theorem that should appear in suggestions
+theorem normalTheorem : True := trivial
+
+-- Define a deprecated theorem that should be filtered out by isDeniedPremise
+@[deprecated "Use normalTheorem instead" (since := "1970-01-01")]
+theorem deprecatedTheorem : True := trivial
+
+-- Another normal theorem to verify filtering is selective
+theorem anotherNormalTheorem : 1 + 1 = 2 := rfl
+
+-- Test the currentFile selector which uses isDeniedPremise to filter
+set_library_suggestions Lean.LibrarySuggestions.currentFile
+
+-- This test verifies that deprecated theorems are filtered out by isDeniedPremise
+-- Expected: deprecatedTheorem should NOT appear in suggestions
+/--
+info: Library suggestions:
+  anotherNormalTheorem
+  normalTheorem
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial