feat: type doc right below initial type naming

leanprover · Nov 13, 2023 · 96147ea · 96147ea
1 parent d70c8b7
commit 96147ea
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
@@ -133,8 +133,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
         [leanInkHtml]
         [attrsHtml]
         {← docInfoHeader doc}
-        [docInfoHtml]
         [docStringHtml]
+        [docInfoHtml]
         [extraInfoHtml]
       </div>
     </div>