Commit 2023-09-13 01:17 2a9e72b4

View on Github →

chore: fix lake exe graph --exclude-meta (#6958)

Estimated changes

Modified ImportGraph/Main.lean

Modified Mathlib/Util/Imports.lean

deleted def Lean.NameMap.dependenciesOf

added def Lean.NameMap.downstreamOf

added def Lean.NameMap.filterGraph

added def Lean.NameMap.transitiveFilteredUpstream

added def Lean.NameMap.upstreamOf