From f4433f3147aea7608d33ae75da2efb33657e157c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Aug 2021 14:27:05 -0700
Subject: [PATCH] =?UTF-8?q?feat:=20add=20`Alternative=20(StateRefT'=20?=
 =?UTF-8?q?=CF=89=20=CF=83=20m)`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Init/Control/StateRef.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index e9c6da9620..7c4e92f3bc 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -32,6 +32,7 @@ variable {ω σ : Type} {m : Type → Type} {α : Type}
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
 instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
+instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
 
 @[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
   fun ref => ref.get
@@ -42,16 +43,14 @@ instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstance
 @[inline] protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
   fun ref => ref.modifyGet f
 
-instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) := {
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
   get       := StateRefT'.get
   set       := StateRefT'.set
   modifyGet := StateRefT'.modifyGet
-}
 
-instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateRefT' ω σ m) := {
+instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateRefT' ω σ m) where
   throw    := StateRefT'.lift ∘ throwThe ε
   tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
-}
 
 end StateRefT'