Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.suggest.head_symbol_match.to_string

Modification history

2019-10-20 10:46
src/tactic/suggest.lean
feat(tactic/suggest): generalize and reimplement library_search (#1552) …
Added tactic.suggest.head_symbol_match.to_stringView on Github →