chore: correct lifting constraints

leanprover · Jul 13, 2024 · a9949bf · a9949bf
1 parent 5b01e7c
commit a9949bf
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git 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
@@ -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