From 8e4b7bdb508e2803c819e89b79a1367d600d9281 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 19 May 2022 21:52:54 +0200
Subject: [PATCH] doc: Output.Structure

---
 DocGen4/Output/Structure.lean | 6 ++++++
 1 file changed, 6 insertions(+)

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
         <div class="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
       </li>
 
+/--
+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