structure CollectAxiomBlame.State : Type

• visited : Lean.NameSet
• axioms : Lean.NameMap (List Lean.Name)

@[reducible, inline]

abbrev CollectAxiomBlame.M (α : Type) : Type

Equations

• CollectAxiomBlame.M = ReaderT Lean.Environment (StateM CollectAxiomBlame.State)

partial def CollectAxiomBlame.collect (src : List Lean.Name) (c : Lean.Name) : CollectAxiomBlame.M Unit

def «command#axiom_blame_» : Lean.ParserDescr

Equations

• «command#axiom_blame_» = Lean.ParserDescr.node `command#axiom_blame_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#axiom_blame ") (Lean.ParserDescr.const `ident))