structure Lean.CollectAxioms.State : Type

• visited : Lean.NameSet
• axioms : Array Lean.Name

@[reducible, inline]

abbrev Lean.CollectAxioms.M (α : Type) : Type

partial def Lean.CollectAxioms.collect (c : Lean.Name) : Lean.CollectAxioms.M Unit

def Lean.collectAxioms {m : Type → Type} [Monad m] [Lean.MonadEnv m] (constName : Lean.Name) : m (Array Lean.Name)