From 1eda0fd7349d282e2e9103f66caf870fe0d751a3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Oct 2022 20:38:06 -0700
Subject: [PATCH] chore: missing annotation

---
 src/Init/Control/Reader.lean | 1 +
 1 file changed, 1 insertion(+)

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)