diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 97414d5..e7ec326 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -81,7 +81,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i) | _ => nodes := nodes - nodes := nodes.push : + nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"] nodes := nodes.push
[←infoFormatToHtml doc.getType]
pure
[nodes]