diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index a51031a..419891d 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -12,7 +12,7 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do pure
  • {shortName} : [←infoFormatToHtml i.type]
  • def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do - let constructorsHtml := + let constructorsHtml := pure #[constructorsHtml] end Output diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 480f3b3..7d00102 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -27,7 +27,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let fileNodes ← (files.mapM moduleListFile) let moduleLink ← moduleNameToLink h.getName pure -