def DeclAudit.allowedAxioms : Std.HashSet Lean.Name

Equations

• DeclAudit.allowedAxioms = ((Std.HashSet.emptyWithCapacity.insert `propext).insert `Classical.choice).insert `Quot.sound

structure DeclAudit.AxiomCache : Type

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

@[reducible, inline]

abbrev DeclAudit.AxiomM (α : Type) : Type

Equations

• DeclAudit.AxiomM = StateT DeclAudit.AxiomCache Lean.MetaM

partial def DeclAudit.collectAxiomDeps (name : Lean.Name) : AxiomM (Array Lean.Name)

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

Equations

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

def DeclAudit.dumpDeclAxioms (modulePrefix : String) (onlyBad : Bool := true) : Lean.MetaM Unit

Equations

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