Do the same for inductives

2023-08-18 08:40:27 +01:00 · 2023-08-18 08:40:27 +01:00 · d3d67c1d92
parent e5ff71991d
commit d3d67c1d92
1 changed files with 1 additions and 1 deletions
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@ -22,8 +22,8 @@ def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
    let renderedDoc ← docStringToHtml doc
    pure
      <li class="constructor" id={name}>
-        <div class="inductive_ctor_doc">[renderedDoc]</div>
        {shortName} : [← infoFormatToHtml c.type]
+        <div class="inductive_ctor_doc">[renderedDoc]</div>
      </li>
  else
    pure