Def Mathlib.Tactic.LibrarySearch.lines

Modification history

2023-04-18 10:28
Mathlib/Tactic/LibrarySearch.lean
chore: refactor of library_search, and don't timeout (#3228) …
Deleted Mathlib.Tactic.LibrarySearch.linesView on Github →
2022-11-03 22:33
Mathlib/Tactic/LibrarySearch.lean
chore: update std4 11-03 (#535) …
Added Mathlib.Tactic.LibrarySearch.linesView on Github →