diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2eddfbc..752f4ed 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -30,7 +30,6 @@ def getCurrentName : HtmlM (Option Name) := do (←read).currentName def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base --- TODO: Change this to HtmlM and auto add the root URl def moduleNameToLink (n : Name) : HtmlM String := do let parts := n.components.map Name.toString (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 91d28ab..37fade1 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -64,7 +64,6 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do nodes := nodes.push : nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) - -- TODO: The final type of the declaration return
[nodes]
def docInfoToHtml (doc : DocInfo) : HtmlM Html := do diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 42f4e35..cc62467 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -150,7 +150,6 @@ def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type | _ => panic! s!"Constructor {ctor} was requested but does not exist" --- TODO: Obtain parameters that come after the inductive Name def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv