chore: fix missing import in Std.Tactic.LibrarySearch (#541)

leanprover-community · Jan 18, 2024 · 1972e07 · 1972e07
1 parent ee4a0f1
commit 1972e07
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Std/Tactic/LibrarySearch.lean b/Std/Tactic/LibrarySearch.lean
@@ -7,6 +7,7 @@ import Std.Lean.CoreM
 import Std.Lean.Expr
 import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.LazyDiscrTree
+import Std.Data.Option.Basic
 import Std.Tactic.SolveByElim
 import Std.Util.Pickle