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

chore: Remove obsolete TODOs

main
Henrik Böving 2022-01-06 02:05:23 +01:00
parent 8a58752c56
commit f71b2ee8b9
3 changed files with 0 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
DocGen4/Output/Base.lean
View File

@ -30,7 +30,6 @@ def getCurrentName : HtmlM (Option Name) := do (←read).currentName
def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
new >>= base new >>= base
-- TODO: Change this to HtmlM and auto add the root URl
def moduleNameToLink (n : Name) : HtmlM String := do def moduleNameToLink (n : Name) : HtmlM String := do
let parts := n.components.map Name.toString let parts := n.components.map Name.toString
(←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"

1
DocGen4/Output/Module.lean
View File

@ -64,7 +64,6 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
nodes := nodes.push <span «class»="decl_args">:</span> nodes := nodes.push <span «class»="decl_args">:</span>
nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
-- TODO: The final type of the declaration
return <div «class»="decl_header"> [nodes] </div> return <div «class»="decl_header"> [nodes] </div>
def docInfoToHtml (doc : DocInfo) : HtmlM Html := do def docInfoToHtml (doc : DocInfo) : HtmlM Html := do

1
DocGen4/Process.lean
View File

@ -150,7 +150,6 @@ def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
| some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type
| _ => panic! s!"Constructor {ctor} was requested but does not exist" | _ => 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 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
let info ← Info.ofConstantVal v.toConstantVal let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv let env ← getEnv