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 aniff
, 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%")