diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean index 2dc6ea3e1a..bf5e3cd7b8 100644 --- a/Lake/BuildMonad.lean +++ b/Lake/BuildMonad.lean @@ -52,9 +52,6 @@ end BuildMethodsRef -- # Build Monad Utilities -------------------------------------------------------------------------------- --- Ideally, this instance would be in the Lean core -instance [Pure m] : MonadLiftT Id m := ⟨pure⟩ - namespace BuildContext deriving instance Inhabited for BuildContext