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

TODO: I suspect this is slow. Either run this at LaTeX output time rather than during @[blueprint] tagging (in which case we can't check for cyclic dependencies), or use some caching (map from declaration to used blueprint nodes).

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.