diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean index 1b8fff7604..4a3fa71437 100644 --- a/src/Init/Control/Reader.lean +++ b/src/Init/Control/Reader.lean @@ -31,6 +31,7 @@ instance : MonadControl m (ReaderT ρ m) where liftWith f ctx := f fun x => x ctx restoreM x _ := x +@[alwaysInline] instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)