HepLean Documentation

Mathlib.Tactic.Find

The #find command and tactic. #

The #find command finds definitions & lemmas using pattern matching on the type. For instance:

#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat

Inside tactic proofs, there is a #find tactic with the same syntax, or the find tactic which looks for lemmas which are applyable against the current goal.

source
opaque Mathlib.Tactic.Find.findDeclsPerHead :
Batteries.Tactic.DeclCache (Std.HashMap Lean.HeadIndex (Array Lean.Name))
source
def Mathlib.Tactic.Find.findType (t : Lean.Expr) :
Lean.Elab.TermElabM Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Tactic.Find.«command#find_» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Mathlib.Tactic.Find.tacticFind :
      Lean.ParserDescr
      Equations
      Instances For
        source
        def Mathlib.Tactic.Find.«tactic#find_» :
        Lean.ParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For