From c31aef8e87b3e7e78aa7a5001ea0308f66f244c8 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sat, 19 Feb 2022 01:54:20 +0800 Subject: [PATCH] fix: remove redundant link to parent module --- DocGen4/Output/Navbar.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 008ebdf..1b8a530 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -21,7 +21,8 @@ def moduleListFile (file : Name) : HtmlM Html := do partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) let dirs := children.filter (λ c => c.getChildren.toList.length != 0) - let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName + let files := children.filter (λ c => Hierarchy.isFile c ∧ c.getChildren.toList.length = 0) + |>.map Hierarchy.getName let dirNodes ← (dirs.mapM moduleListDir) let fileNodes ← (files.mapM moduleListFile) let moduleLink ← moduleNameToLink h.getName