diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index fde7d40..3d6eaf3 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -10,9 +10,9 @@ open Lean def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do pure -
+
Instances For - +
def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do diff --git a/static/instances.js b/static/instances.js index fa73c5c..7125ccc 100644 --- a/static/instances.js +++ b/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 += `
  • ${instance}
  • ` + + if (instances.length == 0) { + instanceForList.remove(); + } else { + var innerHTML = ""; + for(var instance of instances) { + const instanceLink = dataCenter.declNameToLink(instance); + innerHTML += `
  • ${instance}
  • `; + } + const instanceEnum = instanceForList.querySelector(".instances-for-enum"); + instanceEnum.innerHTML = innerHTML; } - instanceForList.innerHTML = innerHTML; } } diff --git a/static/style.css b/static/style.css index b10d3e2..e76bf3a 100644 --- a/static/style.css +++ b/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; }