feat: fix #166

DocGen4/Output/Inductive.lean

@@ -10,9 +10,9 @@ open Lean
 
 def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
   pure
-    <details «class»="instances">
+    <details id={s!"instances-for-list-{typeName}"} «class»="instances-for-list">
         <summary>Instances For</summary>
-        <ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
+        <ul class="instances-for-enum"></ul>
     </details>
 
 def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do

static/instances.js

@@ -26,11 +26,17 @@ async function annotateInstancesFor() {
   for (const instanceForList of instanceForLists) {
     const typeName = instanceForList.id.slice("instances-for-list-".length);
     const instances = dataCenter.instancesForType(typeName);
-    var innerHTML = "";
-    for(var instance of instances) {
-      const instanceLink = dataCenter.declNameToLink(instance);
-      innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
+
+    if (instances.length == 0) {
+      instanceForList.remove();
+    } else {
+      var innerHTML = "";
+      for(var instance of instances) {
+        const instanceLink = dataCenter.declNameToLink(instance);
+        innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`;
+      }
+      const instanceEnum = instanceForList.querySelector(".instances-for-enum");
+      instanceEnum.innerHTML = innerHTML;
     }
-    instanceForList.innerHTML = innerHTML;
   }
 }

static/style.css

@@ -676,7 +676,7 @@ main h2, main h3, main h4, main h5, main h6 {
 }
 
 .imports li, code, .decl_header, .attributes, .structure_field_info,
-        .constructor, .instances li, .equation, .structure_ext_ctor {
+        .constructor, .instances li, .instances-for-list li, .equation, .structure_ext_ctor {
     font-size: 16px;
     font-family: 'JuliaMono', monospace;
 }