# Library search #

This file defines a tactic `library_search`

and a term elaborator `library_search%`

that tries to find a lemma
solving the current goal
(subgoals are solved using `solveByElim`

).

```
example : x < x + 1 := library_search%
example : Nat := by library_search
```

Inserts a new key into a discrimination tree,
but only if it is not of the form `#[*]`

or `#[=, *, *, *]`

.

## Equations

- One or more equations did not get rendered due to their size.

- none: Mathlib.Tactic.LibrarySearch.DeclMod
- symm: Mathlib.Tactic.LibrarySearch.DeclMod
- mp: Mathlib.Tactic.LibrarySearch.DeclMod
- mpr: Mathlib.Tactic.LibrarySearch.DeclMod

A "modifier" for a declaration.

`none`

indicates the original declaration,`symm`

indicates that (possibly after binders) the declaration is an`=`

, and we want to consider the symmetric version,`mp`

indicates that (possibly after binders) the declaration is an`iff`

, and we want to consider the forward direction,`mpr`

similarly, but for the backward direction.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

Shortcut for calling `solveByElim`

.

## Equations

- One or more equations did not get rendered due to their size.

Try to solve the goal either by:

- calling
`solveByElim`

- or applying a library lemma then calling
`solveByElim`

on the resulting goals.

If it successfully closes the goal, returns `none`

.
Otherwise, it returns `some a`

, where `a : Array (MetavarContext × List MVarId)× List MVarId)`

,
with an entry for each library lemma which was successfully applied,
containing the metavariable context after the application, and a list of the subsidiary goals.

(Always succeeds, and the metavariable context stored in the monad is reverted, unless the goal was completely solved.)

(Note that if `solveByElim`

solves some but not all subsidiary goals,
this is not currently tracked.)

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- Mathlib.Tactic.LibrarySearch.«termLibrary_search%» = Lean.ParserDescr.node `Mathlib.Tactic.LibrarySearch.termLibrary_search% 1024 (Lean.ParserDescr.symbol "library_search%")