diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index e514b20..d69f311 100644 --- a/DocGen4/Output/Class.lean +++ b/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 +
  • {name.toString}
  • + +def instancesToHtml (i : ClassInfo) : HtmlM Html := do + let instancesHtml ← i.instances.mapM instanceToHtml + return
    + Instances + +
    def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do - structureToHtml i.toStructureInfo + (←structureToHtml i.toStructureInfo).push (←instancesToHtml i) end Output end DocGen4 diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index cc62467..19f6c2a 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -63,8 +63,7 @@ structure StructureInfo extends Info where deriving Inhabited structure ClassInfo extends StructureInfo where - hasOutParam : Bool - instances : Array CodeWithInfos + instances : Array Name 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 (hasOutParams (←getEnv) v.name) insts_stx + return ClassInfo.mk sinfo (insts.map Expr.constName!) namespace DocInfo