Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-28 22:11 a4fd55ca

View on Github →

feat(library_search): a simple library_search function (#839)

Estimated changes

Modified docs/tactics.md

Modified src/tactic/basic.lean

Modified src/tactic/interactive.lean

Created src/tactic/library_search.lean

added def tactic.library_search.head_symbol_match.to_string

added inductive tactic.library_search.head_symbol_match

Created test/library_search/basic.lean

Created test/library_search/ring_theory.lean