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
ink
opaque Mathlib.Tactic.Find.findDeclsPerHead :
Mathlib.Tactic.DeclCache (Lean.HashMap Lean.HeadIndex (Array Lean.Name))
source
ink
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.
source
ink
def Mathlib.Tactic.Find.«command#find_» :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.Find.tacticFind :
Lean.ParserDescr
Equations
source
ink
def Mathlib.Tactic.Find.«tactic#find_» :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.