diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 5d6a1e7d..a15113dd 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -156,7 +156,7 @@ This is untyped so HtmlM and BaseHtmlM can be mixed. def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β := new >>= base -def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β := +def templateLiftExtends {α β} {m n} [Bind m] [MonadLiftT n m] (base : α → n β) (new : m α) : m β := new >>= (monadLift ∘ base) /-- Returns the doc-gen4 link to a module name. diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index a9b822ee..226bdbfc 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -199,9 +199,6 @@ def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBas let relevantMembers := module.members.filter Process.ModuleMember.shouldRender let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name) let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName - letI : MonadLift BaseHtmlM HtmlM := { - monadLift := fun x => do return x.run (← readThe SiteBaseContext) - } templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[ ← internalNav memberNames module.name, Html.element "main" false #[] memberDocs