feat: list instances of classes

DocGen4/Output/Class.lean

@@ -5,9 +5,22 @@ namespace DocGen4
 namespace Output
 
 open scoped DocGen4.Jsx
+open Lean
+
+def instanceToHtml (name : Name) : HtmlM Html := do
+  <li><a href={←declNameToLink name}>{name.toString}</a></li>
+
+def instancesToHtml (i : ClassInfo) : HtmlM Html := do
+  let instancesHtml ← i.instances.mapM instanceToHtml
+  return <details «class»="instances">
+        <summary>Instances</summary>
+        <ul>
+          [instancesHtml]
+        </ul>
+    </details>
 
 def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
-  structureToHtml i.toStructureInfo
+  (←structureToHtml i.toStructureInfo).push (←instancesToHtml i)
 
 end Output
 end DocGen4

DocGen4/Process.lean

@@ -63,8 +63,7 @@ structure StructureInfo extends Info where
   deriving Inhabited
 
 structure ClassInfo extends StructureInfo where
-  hasOutParam : Bool
+  instances : Array Name
-  instances : Array CodeWithInfos
   deriving Inhabited
 
 inductive DocInfo where
@@ -193,8 +192,7 @@ def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
   let fn ← mkConstWithFreshMVarLevels v.name
   let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
   let insts ← SynthInstance.getInstances (mkAppN fn xs)
-  let insts_stx ← insts.mapM prettyPrintTerm
+  return ClassInfo.mk sinfo (insts.map Expr.constName!)
-  return ClassInfo.mk sinfo (hasOutParams (←getEnv) v.name) insts_stx
 
 namespace DocInfo