This is similar to Lean's collectAxioms, but collects nodes in the blueprint (plus all axioms) rather than just axioms.

structure Architect.CollectUsed.Context : Type

• env : Lean.Environment
• root : Lean.Name

structure Architect.CollectUsed.State : Type

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

@[reducible, inline]

abbrev Architect.CollectUsed.M (α : Type) : Type

Equations

• Architect.CollectUsed.M = ReaderT Architect.CollectUsed.Context (StateM Architect.CollectUsed.State)

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

def Architect.collectUsed {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (constName : Lean.Name) : m (Lean.NameSet × Lean.NameSet)

Returns the irreflexive transitive set of blueprint nodes that a constant depends on, as a pair of sets (constants used by type, constants used by value). They are made disjoint except that possibly both contain sorryAx.

Equations

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