merge master

Author: kim-em

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.Elab.ElabRules
 public import Lean.Elab.Tactic.Simp
 public import Lean.Meta.Tactic.TryThis
-public import Lean.PremiseSelection.Basic
+public import Lean.LibrarySuggestions.Basic
 
 public section
 
@@ -56,7 +56,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
       if let some a := args then a.getElems else #[]
     if config.suggestions then
       -- Get premise suggestions from the premise selector
-      let suggestions ← Lean.PremiseSelection.select (← getMainGoal)
+      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
       -- Convert suggestions to simp argument syntax and add them to the args
       for sugg in suggestions do
         let arg ← `(Parser.Tactic.simpLemma| $(mkIdent sugg.name):term)
@@ -91,7 +91,7 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
       if let some a := args then a.getElems else #[]
     if config.suggestions then
       -- Get premise suggestions from the premise selector
-      let suggestions ← Lean.PremiseSelection.select (← getMainGoal)
+      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
       -- Convert suggestions to simp argument syntax and add them to the args
       for sugg in suggestions do
         let arg ← `(Parser.Tactic.simpLemma| $(mkIdent sugg.name):term)

tests/lean/run/simp_suggestions.lean

@@ -1,4 +1,4 @@
-import Lean.PremiseSelection
+import Lean.LibrarySuggestions
 
 -- A custom function that simp doesn't know about
 def myCustomAdd (x y : Nat) : Nat := x + y
@@ -8,7 +8,7 @@ theorem myCustomAdd_comm (x y : Nat) : myCustomAdd x y = myCustomAdd y x := by
   simp [myCustomAdd, Nat.add_comm]
 
 -- Set up a premise selector that suggests our helper theorem
-set_premise_selector (fun _ _ => pure #[{ name := `myCustomAdd_comm, score := 1.0 }])
+set_library_suggestions (fun _ _ => pure #[{ name := `myCustomAdd_comm, score := 1.0 }])
 
 -- Test that regular simp? fails without the premise
 example (a b : Nat) : myCustomAdd a b = myCustomAdd b a := by