Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.library_search.head_symbol_match.to_string

Modification history

2019-10-20 10:46
src/tactic/library_search.lean
feat(tactic/suggest): generalize and reimplement library_search (#1552) …
Deleted tactic.library_search.head_symbol_match.to_stringView on Github →
2019-03-28 22:11
src/tactic/library_search.lean
feat(library_search): a simple library_search function (#839)
Added tactic.library_search.head_symbol_match.to_stringView on Github →