Incremental Library Search (#421)

This ports library_search from Mathlib to Std.  It preserves the ability to do caching, but is designed to support a cacheless mode.  The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Std.lean

@@ -62,6 +62,7 @@ import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.Expr
 import Std.Lean.Meta.Inaccessible
 import Std.Lean.Meta.InstantiateMVars
+import Std.Lean.Meta.LazyDiscrTree
 import Std.Lean.Meta.SavedState
 import Std.Lean.Meta.Simp
 import Std.Lean.Meta.UnusedNames
@@ -100,6 +101,7 @@ import Std.Tactic.HaveI
 import Std.Tactic.Instances
 import Std.Tactic.LabelAttr
 import Std.Tactic.LeftRight
+import Std.Tactic.LibrarySearch
 import Std.Tactic.Lint
 import Std.Tactic.Lint.Basic
 import Std.Tactic.Lint.Frontend

Std/Lean/Meta/Basic.lean

@@ -457,3 +457,20 @@ def getLocalHyps [Monad m] [MonadLCtx m] : m (Array Expr) := do
   for d in ← getLCtx do
     if !d.isImplementationDetail then hs := hs.push d.toExpr
   return hs
+
+/--
+Given a monadic function `F` that takes a type and a term of that type and produces a new term,
+lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
+and then builds the lambda telescope term for the new term.
+-/
+def mapForallTelescope' (F : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
+  forallTelescope (← Meta.inferType forallTerm) fun xs ty => do
+    Meta.mkLambdaFVars xs (← F ty (mkAppN forallTerm xs))
+
+/--
+Given a monadic function `F` that takes a term and produces a new term,
+lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
+and then builds the lambda telescope term for the new term.
+-/
+def mapForallTelescope (F : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
+  mapForallTelescope' (fun _ e => F e) forallTerm