diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 4a73bd3..47dbcaa 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -7,10 +7,21 @@ namespace Output
open scoped DocGen4.Jsx
-def ctorToHtml (i : Process.NameInfo) : HtmlM Html := do
- let shortName := i.name.components'.head!.toString
- let name := i.name.toString
- pure
{shortName} : [←infoFormatToHtml i.type]
+def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
+ let shortName := c.name.components'.head!.toString
+ let name := c.name.toString
+ if let some doc := c.doc then
+ let renderedDoc ← docStringToHtml doc
+ pure
+
+ [renderedDoc]
+ {shortName} : [←infoFormatToHtml c.type]
+
+ else
+ pure
+
+ {shortName} : [←infoFormatToHtml c.type]
+
def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
let constructorsHtml := [← i.ctors.toArray.mapM ctorToHtml]
diff --git a/static/style.css b/static/style.css
index 85d0362..fbf8614 100644
--- a/static/style.css
+++ b/static/style.css
@@ -491,6 +491,11 @@ pre code { padding: 0 0; }
margin-left: 2ex;
}
+.inductive_ctor_doc {
+ text-indent: 2ex;
+ padding-top: 1ex;
+}
+
.structure_field_doc {
text-indent: 0;
padding-top: 1ex;