def DeclAudit.hashString {α : Sort u} [Hashable α] (a : α) : String

Equations

• DeclAudit.hashString a = toString (hash a)

def DeclAudit.bodyHashString (info : Lean.ConstantInfo) : String

Equations

• DeclAudit.bodyHashString (Lean.ConstantInfo.defnInfo v) = DeclAudit.hashString v.value
• DeclAudit.bodyHashString (Lean.ConstantInfo.thmInfo val) = "<proof-skipped>"
• DeclAudit.bodyHashString (Lean.ConstantInfo.opaqueInfo v) = DeclAudit.hashString v.value
• DeclAudit.bodyHashString (Lean.ConstantInfo.axiomInfo val) = "<axiom>"
• DeclAudit.bodyHashString (Lean.ConstantInfo.inductInfo v) = toString "<ctors:" ++ toString (DeclAudit.formatNames v.ctors.toArray) ++ toString ">"
• DeclAudit.bodyHashString (Lean.ConstantInfo.ctorInfo val) = "<ctor>"
• DeclAudit.bodyHashString (Lean.ConstantInfo.recInfo val) = "<recursor>"
• DeclAudit.bodyHashString (Lean.ConstantInfo.quotInfo val) = "<quot>"

def DeclAudit.projectConstantsInExpr (projectDecls : Std.HashSet Lean.Name) (self : Lean.Name) (expr : Lean.Expr) : Array Lean.Name

Equations

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

def DeclAudit.collectProjectSpecDeps (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.SpecClosureCache : Type

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

@[reducible, inline]

abbrev DeclAudit.SpecClosureM (α : Type) : Type

Equations

• DeclAudit.SpecClosureM = ReaderT (Std.HashSet Lean.Name) (StateT DeclAudit.SpecClosureCache Lean.MetaM)

partial def DeclAudit.collectSpecClosureFromDecl (name : Lean.Name) : SpecClosureM (Array Lean.Name)

def DeclAudit.targetTypeProjectDeps (projectDecls : Std.HashSet Lean.Name) (target : Lean.Name) : Lean.MetaM (Array Lean.Name)

Equations

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

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

Equations

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

def DeclAudit.depsField (deps : Array Lean.Name) : String

Equations

• DeclAudit.depsField deps = ",".intercalate (Array.map (fun (n : Lean.Name) => n.toString) deps).toList

def DeclAudit.printDeclHashTsv (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.dumpSpecClosureBodyHashes (modulePrefix : String) (target : Lean.Name) : Lean.MetaM Unit

Equations

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

def DeclAudit.mixDeclSpecHash (name : Lean.Name) (info : Lean.ConstantInfo) : UInt64

Equations

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

def DeclAudit.specClosureHash (modulePrefix : String) (target : Lean.Name) : Lean.MetaM (UInt64 × ℕ)

Equations

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

def DeclAudit.dumpSpecClosureHash (modulePrefix : String) (target : Lean.Name) : Lean.MetaM Unit

Equations

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