Def Lean.NameMap.filterGraph

Modification history

2024-01-10 11:53
Mathlib/Util/Imports.lean
refactor: split `ImportGraph` into its own package. (#9169) …
Deleted Lean.NameMap.filterGraphView on Github →
2023-09-13 01:17
Mathlib/Util/Imports.lean
chore: fix lake exe graph --exclude-meta (#6958)
Added Lean.NameMap.filterGraphView on Github →