diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 0afeaf6..fde7d40 100644 --- 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
  • -
    [renderedDoc]
    {shortName} : [← infoFormatToHtml c.type] +
    [renderedDoc]
  • else pure