r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: Readd equations for instances

main
Henrik Böving 2022-02-20 13:52:57 +01:00
parent b87c1cc1de
commit a86c384354
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
DocGen4/Output/Module.lean
View File

@ -89,6 +89,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
let extraInfoHtml ← match doc with let extraInfoHtml ← match doc with
| DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances] | DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances]
| DocInfo.definitionInfo i => equationsToHtml i | DocInfo.definitionInfo i => equationsToHtml i
| DocInfo.instanceInfo i => equationsToHtml i
| DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances] | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances]
| i => pure #[] | i => pure #[]
let attrs := doc.getAttrs let attrs := doc.getAttrs