Def Lean.NameMap.dependenciesOf

Modification history

2023-09-13 01:17
Mathlib/Util/Imports.lean
chore: fix lake exe graph --exclude-meta (#6958)
Deleted Lean.NameMap.dependenciesOfView on Github →
2023-07-10 05:24
Mathlib/Util/Imports.lean
feat: `lake exe graph`, as replacement for `leanproject import-graph` (#5513) …
Added Lean.NameMap.dependenciesOfView on Github →