Documentation

Mathlib.Tactic.LibrarySearch

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.

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:

    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.