feat: equations for instances

main
Henrik Böving 2022-02-04 22:48:08 +01:00
parent f54c192e6f
commit 419c1eb1e6
3 changed files with 16 additions and 4 deletions

View File

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

View File

@ -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

View File

@ -8,6 +8,7 @@ import DocGen4.Output.Inductive
import DocGen4.Output.Structure import DocGen4.Output.Structure
import DocGen4.Output.Class import DocGen4.Output.Class
import DocGen4.Output.Definition import DocGen4.Output.Definition
import DocGen4.Output.Instance
namespace DocGen4 namespace DocGen4
namespace Output namespace Output
@ -77,6 +78,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
| DocInfo.structureInfo i => structureToHtml i | DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i | DocInfo.classInfo i => classToHtml i
| DocInfo.definitionInfo i => definitionToHtml i | DocInfo.definitionInfo i => definitionToHtml i
| DocInfo.instanceInfo i => instanceToHtml i
| _ => #[] | _ => #[]
return <div «class»="decl" id={doc.getName.toString}> return <div «class»="decl" id={doc.getName.toString}>