From 306959b9216a87fdd60fafe2d0b88f6a2372bd7b Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Tue, 23 May 2023 16:57:16 -0600 Subject: [PATCH] feat: list instances for defs also --- DocGen4/Output/Module.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index dd673e5..03c0fdc 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -98,7 +98,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do -- extra information like equations and instances let extraInfoHtml ← match doc with | DocInfo.classInfo i => pure #[← classInstancesToHtml i.name] - | DocInfo.definitionInfo i => equationsToHtml i + | DocInfo.definitionInfo i => pure ((← equationsToHtml i) ++ #[← instancesForToHtml i.name]) | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo | DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name] | DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]