def DeclAudit.kindOf : Lean.ConstantInfo → String

Equations

• DeclAudit.kindOf (Lean.ConstantInfo.axiomInfo val) = "axiom"
• DeclAudit.kindOf (Lean.ConstantInfo.defnInfo val) = "def"
• DeclAudit.kindOf (Lean.ConstantInfo.thmInfo val) = "theorem"
• DeclAudit.kindOf (Lean.ConstantInfo.opaqueInfo val) = "opaque"
• DeclAudit.kindOf (Lean.ConstantInfo.quotInfo val) = "quot"
• DeclAudit.kindOf (Lean.ConstantInfo.inductInfo val) = "inductive"
• DeclAudit.kindOf (Lean.ConstantInfo.ctorInfo val) = "ctor"
• DeclAudit.kindOf (Lean.ConstantInfo.recInfo val) = "recursor"

def DeclAudit.formatNames (names : Array Lean.Name) : String

Equations

• DeclAudit.formatNames names = "[" ++ ", ".intercalate (Array.map (fun (n : Lean.Name) => n.toString) names).toList ++ "]"

def DeclAudit.oneLine (s : String) : String

Equations

• DeclAudit.oneLine s = s.replace "\n" " "

def DeclAudit.pushName (names : Array Lean.Name) (name : Lean.Name) : Array Lean.Name

Equations

• DeclAudit.pushName names name = if names.contains name = true then names else names.push name

def DeclAudit.mergeNames (xs ys : Array Lean.Name) : Array Lean.Name

Equations

• DeclAudit.mergeNames xs ys = Array.foldl DeclAudit.pushName xs ys

def DeclAudit.nameSetOf (names : Array Lean.Name) : Std.HashSet Lean.Name

Equations

• DeclAudit.nameSetOf names = Array.foldl (fun (acc : Std.HashSet Lean.Name) (name : Lean.Name) => acc.insert name) Std.HashSet.emptyWithCapacity names

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

Equations

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

def DeclAudit.projectDeclSet (modulePrefix : String) : Lean.MetaM (Std.HashSet Lean.Name)

Equations

• DeclAudit.projectDeclSet modulePrefix = do let decls ← DeclAudit.analysisDecls modulePrefix pure (DeclAudit.nameSetOf decls)

def DeclAudit.declSummary (name : Lean.Name) : Lean.MetaM String

Equations

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

def DeclAudit.nodeKind (name : Lean.Name) : Lean.MetaM String

Equations

• DeclAudit.nodeKind name = do let env ← Lean.getEnv match env.find? name with | some info => pure (DeclAudit.kindOf info) | none => pure "unknown"

def DeclAudit.ensureProjectDecl (modulePrefix : String) (projectDecls : Std.HashSet Lean.Name) (name : Lean.Name) : Lean.MetaM Unit

Equations

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

def DeclAudit.getCheckedConst? (name : Lean.Name) : Lean.MetaM (Option Lean.ConstantInfo)

Equations

• DeclAudit.getCheckedConst? name = do let __do_lift ← Lean.getEnv pure (__do_lift.checked.get.find? name)