diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index d69f311..f803a6d 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -7,11 +7,11 @@ namespace Output open scoped DocGen4.Jsx open Lean -def instanceToHtml (name : Name) : HtmlM Html := do +def classInstanceToHtml (name : Name) : HtmlM Html := do
  • {name.toString}
  • -def instancesToHtml (i : ClassInfo) : HtmlM Html := do - let instancesHtml ← i.instances.mapM instanceToHtml +def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do + let instancesHtml ← i.instances.mapM classInstanceToHtml return
    Instances
    def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do - (←structureToHtml i.toStructureInfo).push (←instancesToHtml i) + (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i) end Output end DocGen4 diff --git a/DocGen4/Output/Instance.lean b/DocGen4/Output/Instance.lean new file mode 100644 index 0000000..bad10f1 --- /dev/null +++ b/DocGen4/Output/Instance.lean @@ -0,0 +1,10 @@ +import DocGen4.Output.Template +import DocGen4.Output.Definition + +namespace DocGen4 +namespace Output + +def instanceToHtml (i : InstanceInfo) : HtmlM (Array Html) := definitionToHtml i + +end Output +end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 1a37ae9..d203241 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -8,6 +8,7 @@ import DocGen4.Output.Inductive import DocGen4.Output.Structure import DocGen4.Output.Class import DocGen4.Output.Definition +import DocGen4.Output.Instance namespace DocGen4 namespace Output @@ -77,6 +78,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.structureInfo i => structureToHtml i | DocInfo.classInfo i => classToHtml i | DocInfo.definitionInfo i => definitionToHtml i + | DocInfo.instanceInfo i => instanceToHtml i | _ => #[] return