feat: library suggestion engine for local theorems

Author: kim-em

tests/lean/run/library_suggestions_local.lean

@@ -0,0 +1,39 @@
+import Lean.LibrarySuggestions.Basic
+
+-- Define some initial local constants
+def myLocalDef : Nat := 42
+
+theorem myLocalTheorem : myLocalDef = 42 := rfl
+
+-- Add a theorem in the Lean namespace (should be filtered by isDeniedPremise)
+namespace Lean
+theorem shouldBeFiltered : True := trivial
+end Lean
+
+-- Test the currentFile selector (should only show theorems, not definitions)
+set_library_suggestions Lean.LibrarySuggestions.currentFile
+
+-- First test: should show only myLocalTheorem
+-- (not myLocalDef since it's a def, not Lean.shouldBeFiltered since it's in Lean namespace)
+/--
+info: Library suggestions: [myLocalTheorem]
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial
+
+-- Add more local constants (mix of theorems and definitions)
+theorem anotherTheorem : True := trivial
+
+def myFunction (x : Nat) : Nat := x + 1
+
+-- Second test: should show only the two theorems (not myFunction)
+/--
+info: Library suggestions: [anotherTheorem, myLocalTheorem]
+-/
+#guard_msgs in
+example : False → True := by
+  suggestions
+  intro h
+  trivial