diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index aa0b8d8..fee0d0d 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -7,6 +7,9 @@ namespace Output open scoped DocGen4.Jsx open Lean +/-- +Render a single field consisting of its documentation, its name and its type as HTML. +-/ def fieldToHtml (f : NameInfo) : HtmlM Html := do let shortName := f.name.components'.head!.toString let name := f.name.toString @@ -23,6 +26,9 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
{s!"{shortName} "} : [←infoFormatToHtml f.type]
+/-- +Render all information about a structure as HTML. +-/ def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do let structureHtml := if Name.isSuffixOf `mk i.ctor.name then