def DeclAudit.collectProjectDirectDeps (projectDecls : Std.HashSet Lean.Name) (name : Lean.Name) : Lean.MetaM (Array Lean.Name)

Equations

• One or more equations did not get rendered due to their size.

structure DeclAudit.DependencyCache : Type

• memo : Std.HashMap Lean.Name (Array Lean.Name)
• visiting : Lean.NameSet

@[reducible, inline]

abbrev DeclAudit.DependencyM (α : Type) : Type

Equations

• DeclAudit.DependencyM = ReaderT (Std.HashSet Lean.Name) (StateT DeclAudit.DependencyCache Lean.MetaM)

partial def DeclAudit.collectProjectTransitiveDeps (root name : Lean.Name) : DependencyM (Array Lean.Name)

def DeclAudit.dumpDirectDeps (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveDeps (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpAllDirectDeps (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpAllTransitiveDeps (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.printGraphNodeTsv (name : Lean.Name) : Lean.MetaM Unit

Equations

• DeclAudit.printGraphNodeTsv name = do let __do_lift ← DeclAudit.nodeKind name liftM (IO.println (toString "NODE\t" ++ toString name ++ toString "\t" ++ toString __do_lift))

def DeclAudit.printGraphEdgeTsv (src dst : Lean.Name) : Lean.MetaM Unit

Equations

• DeclAudit.printGraphEdgeTsv src dst = liftM (IO.println (toString "EDGE\t" ++ toString src ++ toString "\t" ++ toString dst))

def DeclAudit.dumpGraphNodesTsv (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpDirectGraphTsv (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveGraphTsv (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpDirectEdgesTsv (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveEdgesTsv (modulePrefix : String) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.transitiveClosureNodesForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM (Array Lean.Name)

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpDirectGraphTsvForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveGraphTsvForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpDirectEdgesTsvForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveEdgesTsvForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveInducedGraphTsvForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def DeclAudit.dumpTransitiveInducedEdgesTsvForDecl (modulePrefix : String) (name : Lean.Name) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.