def DocGen4.getNLevels (name : Lean.Name) (levels : Nat) : Lean.Name

Equations

• DocGen4.getNLevels name levels = List.foldl (fun (x1 x2 : Lean.Name) => x1 ++ x2) Lean.Name.anonymous (List.drop (name.componentsRev.length - levels) name.componentsRev).reverse

inductive DocGen4.Hierarchy : Type

• node (name : Lean.Name) (isFile : Bool) (children : Lean.RBNode Lean.Name fun (x : Lean.Name) => Hierarchy) : Hierarchy

@[implicit_reducible]

instance DocGen4.instInhabitedHierarchy : Inhabited Hierarchy

Equations

• DocGen4.instInhabitedHierarchy = { default := DocGen4.Hierarchy.node Lean.Name.anonymous false Lean.RBNode.leaf }

@[reducible, inline]

abbrev DocGen4.HierarchyMap : Type

Equations

• DocGen4.HierarchyMap = Lean.RBNode Lean.Name fun (x : Lean.Name) => DocGen4.Hierarchy

def DocGen4.HierarchyMap.toList : HierarchyMap → List (Lean.Name × Hierarchy)

Equations

• x✝.toList = Lean.RBNode.revFold (fun (ps : List (Lean.Name × DocGen4.Hierarchy)) (k : Lean.Name) (v : DocGen4.Hierarchy) => (k, v) :: ps) [] x✝

def DocGen4.HierarchyMap.toArray : HierarchyMap → Array (Lean.Name × Hierarchy)

Equations

• x✝.toArray = Lean.RBNode.fold (fun (ps : Array (Lean.Name × DocGen4.Hierarchy)) (k : Lean.Name) (v : DocGen4.Hierarchy) => ps ++ #[(k, v)]) #[] x✝

def DocGen4.HierarchyMap.hForIn {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (t : HierarchyMap) (init : σ) (f : Lean.Name × Hierarchy → σ → m (ForInStep σ)) : m σ

Equations

• t.hForIn init f = Lean.RBNode.forIn t init fun (a : Lean.Name) (b : DocGen4.Hierarchy) (acc : σ) => f (a, b) acc

@[implicit_reducible]

instance DocGen4.HierarchyMap.instForInProdNameHierarchyOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m HierarchyMap (Lean.Name × Hierarchy)

Equations

• DocGen4.HierarchyMap.instForInProdNameHierarchyOfMonad = { forIn := fun {β : Type ?u.2} => DocGen4.HierarchyMap.hForIn }

def DocGen4.Hierarchy.empty (n : Lean.Name) (isFile : Bool) : Hierarchy

Equations

• DocGen4.Hierarchy.empty n isFile = DocGen4.Hierarchy.node n isFile Lean.RBNode.leaf

def DocGen4.Hierarchy.getName : Hierarchy → Lean.Name

Equations

• (DocGen4.Hierarchy.node n isFile children).getName = n

def DocGen4.Hierarchy.getChildren : Hierarchy → HierarchyMap

Equations

• (DocGen4.Hierarchy.node n isFile children).getChildren = children

def DocGen4.Hierarchy.isFile : Hierarchy → Bool

Equations

• (DocGen4.Hierarchy.node n isFile children).isFile = isFile

partial def DocGen4.Hierarchy.insert! (h : Hierarchy) (n : Lean.Name) : Hierarchy

def DocGen4.Hierarchy.fromArray (names : Array Lean.Name) : Hierarchy

Equations

• DocGen4.Hierarchy.fromArray names = Array.foldl DocGen4.Hierarchy.insert! (DocGen4.Hierarchy.empty Lean.Name.anonymous false) names

partial def DocGen4.Hierarchy.contains (h : Hierarchy) (n : Lean.Name) : Bool

Returns true if n was inserted into h as a file (i.e. was one of the names passed to fromArray / insert!). Intermediate "container" nodes that were synthesized to host children but never inserted as files themselves return false.

Used by moduleNameToLink to decide local-vs-external linking: a module present here goes through the relative URL path; anything else falls back to the external documentation site.