source
structure Lean.CollectAxioms.State :
Type

- visited : NameSet
- axioms : Array Name

Instances For

source
@[reducible, inline]
abbrev Lean.CollectAxioms.M (α : Type) :
Type
Equations

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

Instances For

source
partial def Lean.CollectAxioms.collect (c : Name) :
M Unit
source
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

Instances For