diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 8ea1b315ff..93690de4d3 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -869,6 +869,7 @@ class MonadEnv (m : Type → Type) where export MonadEnv (getEnv modifyEnv) +@[alwaysInline] instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where getEnv := liftM (getEnv : m Environment) modifyEnv := fun f => liftM (modifyEnv f : m Unit) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 126475c775..b15fafae8d 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -330,6 +330,7 @@ class MonadMCtx (m : Type → Type) where export MonadMCtx (getMCtx modifyMCtx) +@[alwaysInline] instance (m n) [MonadLift m n] [MonadMCtx m] : MonadMCtx n where getMCtx := liftM (getMCtx : m _) modifyMCtx := fun f => liftM (modifyMCtx f : m _)