structure Lean.CollectAxioms.State : Type

• visited : NameSet
• axioms : Array 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 : Name) : M Unit

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

Equations

• Lean.collectAxioms constName = do let env ← Lean.getEnv match StateT.run (ReaderT.run (Lean.CollectAxioms.collect constName) env) { } with | (fst, s) => pure s.axioms