diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 734bb34..fc13f4e 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -71,7 +71,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
 
   let mut declList := #[]
   for (_, mod) in result.moduleInfo.toArray do
-    for decl in mod.members.filter ModuleMember.isDocInfo do
+    for decl in filterMapDocInfo mod.members do
       let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
       let findDir := basePath / "find" / decl.getName.toString
       FS.createDirAll findDir
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 5d41123..4c76230 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -178,10 +178,11 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
     </nav>
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-  let docInfos ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
+  let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
+  let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName
   templateExtends (baseHtmlArray module.name.toString) $ pure #[
-    ←internalNav (module.members.filter ModuleMember.isDocInfo |>.map ModuleMember.getName) module.name,
-    Html.element "main" false #[] docInfos
+    ←internalNav memberNames module.name,
+    Html.element "main" false #[] memberDocs
   ]
 
 end Output
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 0647fb9..6de8304 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -461,10 +461,6 @@ def getDeclarationRange : ModuleMember → DeclarationRange
 def order (l r : ModuleMember) : Bool :=
   Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos
 
-def isDocInfo : ModuleMember → Bool
-| docInfo _ => true
-| _ => false
-
 def getName : ModuleMember → Name
 | docInfo i => i.getName
 | modDoc i => Name.anonymous
@@ -475,6 +471,13 @@ def getDocString : ModuleMember → Option String
 
 end ModuleMember
 
+def filterMapDocInfo (ms : Array ModuleMember) : Array DocInfo :=
+  ms.filterMap filter
+  where
+    filter : ModuleMember → Option DocInfo
+    | ModuleMember.docInfo i => some i
+    | _ => none
+
 structure AnalyzerResult where
   name2ModIdx : HashMap Name ModuleIdx
   moduleNames : Array Name