structure Lean.CollectAxioms.State : Type

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

@[reducible, inline]

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

Equations

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

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

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

Equations

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