# mathlibdocumentation

tactic.find

meta def expr.get_pis  :
meta def pexpr.get_uninst_pis  :
pexpr
meta def find_cmd (_x : interactive.parse (lean.parser.tk "#find")) :

The find command from tactic.find allows to find definitions lemmas using pattern matching on the type. For instance:

import tactic.find

run_cmd tactic.skip

#find _ + _ = _ + _
#find (_ : ℕ) + _ = _ + _
#find ℕ → ℕ


The tactic library_search is an alternate way to find lemmas in the library.

The find command from tactic.find allows to find definitions lemmas using pattern matching on the type. For instance:

import tactic.find

run_cmd tactic.skip

#find _ + _ = _ + _
#find (_ : ℕ) + _ = _ + _
#find ℕ → ℕ


The tactic library_search is an alternate way to find lemmas in the library.