@[simp]

theorem monadMap_refl {m : Type u_1 → Type u_2} {α : Type u_1} (f : {α : Type u_1} → m α → m α) : monadMap f = f

ExceptT

theorem ExceptT.ext {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ExceptT ε m α} (h : x.run = y.run) : x = y

theorem ExceptT.ext_iff {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ExceptT ε m α} : x = y ↔ x.run = y.run

@[simp]

theorem ExceptT.stM_eq {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] : stM m (ExceptT ε m) α = Except ε α

@[simp]

theorem ExceptT.run_mk {m : Type (max u_1 u_2) → Type u_3} {ε α : Type (max u_1 u_2)} (x : m (Except ε α)) : (mk x).run = x

@[simp]

theorem ExceptT.run_pure {m : Type u_1 → Type u_2} {α ε : Type u_1} [Monad m] (x : α) : (pure x).run = pure (Except.ok x)

@[simp]

theorem ExceptT.run_lift {m : Type u → Type v} {α ε : Type u} [Monad m] (x : m α) : (ExceptT.lift x).run = Except.ok <$> x

@[simp]

theorem ExceptT.run_throw {m : Type u_1 → Type u_2} {ε β : Type u_1} {e : ε} [Monad m] : (throw e).run = pure (Except.error e)

@[simp]

theorem ExceptT.run_bind_lift {m : Type u_1 → Type u_2} {α ε β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : (ExceptT.lift x >>= f).run = do let a ← x (f a).run

@[simp]

theorem ExceptT.bind_throw {m : Type u_1 → Type u_2} {α ε β : Type u_1} {e : ε} [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : throw e >>= f = throw e

theorem ExceptT.run_bind {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β) : (x >>= f).run = do let x ← x.run match x with | Except.ok x => (f x).run | Except.error e => pure (Except.error e)

@[simp]

theorem ExceptT.lift_pure {m : Type u_1 → Type u_2} {α ε : Type u_1} [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = pure a

@[simp]

theorem ExceptT.run_map {m : Type u_1 → Type u_2} {α β ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : (f <$> x).run = Except.map f <$> x.run

@[simp]

theorem ExceptT.run_monadMap {n : Type u → Type u_1} {m : Type u → Type u_2} {ε α : Type u} [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ExceptT ε m α) : (monadMap f x).run = monadMap f x.run

theorem ExceptT.seq_eq {m : Type u → Type u_1} {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = do let f ← mf f <$> x

theorem ExceptT.bind_pure_comp {m : Type u_1 → Type u_2} {α β ε : Type u_1} [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x

theorem ExceptT.seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = Function.const β <$> x <*> y

theorem ExceptT.seqRight_eq {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = Function.const α id <$> x <*> y

instance ExceptT.instLawfulMonad {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m)

@[simp]

theorem ExceptT.map_throw {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] {α β : Type u_1} (f : α → β) (e : ε) : f <$> throw e = throw e

Note that the MonadControl instance for ExceptT is not monad-generic.

@[simp]

theorem ExceptT.run_restoreM {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] (x : stM m (ExceptT ε m) α) : (restoreM x).run = pure x

@[simp]

theorem ExceptT.run_liftWith {m : Type u → Type u_1} {ε α : Type u} [Monad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m α) : (liftWith f).run = Except.ok <$> f fun {β : Type u} (x : ExceptT ε m β) => x.run

@[simp]

theorem ExceptT.run_controlAt {m : Type u → Type u_1} {ε α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) : (controlAt m f).run = f fun {β : Type u} (x : ExceptT ε m β) => x.run

@[simp]

theorem ExceptT.run_control {m : Type u → Type u_1} {ε α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) : (control f).run = f fun {β : Type u} (x : ExceptT ε m β) => x.run

@[simp]

theorem ExceptT.run_adapt {m : Type u_1 → Type u_2} {ε ε' α : Type u_1} [Monad m] (f : ε → ε') (x : ExceptT ε m α) : (ExceptT.adapt f x).run = Except.mapError f <$> x.run

theorem ExceptT.run_tryCatch {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (h : ε → ExceptT ε m α) : (tryCatch x h).run = do let r ← x.run match r with | Except.ok a => pure (Except.ok a) | Except.error e => (h e).run

@[simp]

theorem ExceptT.run_liftM {α ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : m α) : (liftM x).run = Except.ok <$> x

theorem ExceptT.run_orElse {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (h : Unit → ExceptT ε m α) : (OrElse.orElse x h).run = do let r ← x.run match r with | Except.ok a => pure (Except.ok a) | Except.error a => (h ()).run

Except

instance instLawfulMonadExcept {ε : Type u_1} : LawfulMonad (Except ε)

instance instLawfulApplicativeExcept {ε : Type u_1} : LawfulApplicative (Except ε)

instance instLawfulFunctorExcept {ε : Type u_1} : LawfulFunctor (Except ε)

OptionT

theorem OptionT.ext {m : Type u_1 → Type u_2} {α : Type u_1} {x y : OptionT m α} (h : x.run = y.run) : x = y

theorem OptionT.ext_iff {m : Type u_1 → Type u_2} {α : Type u_1} {x y : OptionT m α} : x = y ↔ x.run = y.run

@[simp]

theorem OptionT.run_mk {α : Type u} {m : Type u → Type v} (x : m (Option α)) : (OptionT.mk x).run = x

@[simp]

theorem OptionT.run_pure {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : α) : (pure x).run = pure (some x)

@[simp]

theorem OptionT.run_lift {m : Type u → Type v} {α : Type u} [Monad m] (x : m α) : (OptionT.lift x).run = do let __do_lift ← x pure (some __do_lift)

@[simp]

theorem OptionT.run_throw {m : Type u_1 → Type u_2} {β : Type u_1} {e : PUnit} [Monad m] : (throw e).run = pure none

@[simp]

theorem OptionT.run_bind_lift {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → OptionT m β) : (OptionT.lift x >>= f).run = do let a ← x (f a).run

@[simp]

theorem OptionT.bind_throw {m : Type u_1 → Type u_2} {α β : Type u_1} {e : PUnit} [Monad m] [LawfulMonad m] (f : α → OptionT m β) : throw e >>= f = throw e

@[simp]

theorem OptionT.run_bind {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {x : OptionT m α} (f : α → OptionT m β) [Monad m] : (x >>= f).run = Option.elimM x.run (pure none) fun (x : α) => (f x).run

@[simp]

theorem OptionT.lift_pure {m : Type u → Type u_1} [Monad m] [LawfulMonad m] {α : Type u} (a : α) : OptionT.lift (pure a) = pure a

@[simp]

theorem OptionT.run_map {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : OptionT m α) : (f <$> x).run = Option.map f <$> x.run

@[simp]

theorem OptionT.run_monadMap {n : Type u → Type u_1} {m : Type u → Type u_2} {α : Type u} [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : OptionT m α) : (monadMap f x).run = monadMap f x.run

theorem OptionT.seq_eq {m : Type u → Type u_1} {α β : Type u} [Monad m] (mf : OptionT m (α → β)) (x : OptionT m α) : mf <*> x = do let f ← mf f <$> x

theorem OptionT.bind_pure_comp {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] (f : α → β) (x : OptionT m α) : x >>= pure ∘ f = f <$> x

theorem OptionT.seqLeft_eq {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x <* y = Function.const β <$> x <*> y

theorem OptionT.seqRight_eq {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x *> y = Function.const α id <$> x <*> y

instance OptionT.instLawfulMonad {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m)

@[simp]

theorem OptionT.run_seq {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) : (f <*> x).run = Option.elimM f.run (pure none) fun (f : α → β) => Option.map f <$> x.run

@[simp]

theorem OptionT.run_seqLeft {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : (x <* y).run = Option.elimM x.run (pure none) fun (x : α) => Option.map (Function.const β x) <$> y.run

@[simp]

theorem OptionT.run_seqRight {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run)

@[simp]

theorem OptionT.run_failure {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] : failure.run = pure none

@[simp]

theorem OptionT.map_failure {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {α β : Type u_1} (f : α → β) : f <$> failure = failure

@[simp]

theorem OptionT.run_orElse {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x y : OptionT m α) : (x <|> y).run = Option.elimM x.run y.run fun (x : α) => pure (some x)

Note that the MonadControl instance for OptionT is not monad-generic.

@[simp]

theorem OptionT.run_restoreM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : stM m (OptionT m) α) : (restoreM x).run = pure x

@[simp]

theorem OptionT.run_liftWith {m : Type u → Type u_1} {α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m α) : (liftWith f).run = some <$> f fun {β : Type u} (x : OptionT m β) => x.run

@[simp]

theorem OptionT.run_controlAt {m : Type u → Type u_1} {α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) : (controlAt m f).run = f fun {β : Type u} (x : OptionT m β) => x.run

@[simp]

theorem OptionT.run_control {m : Type u → Type u_1} {α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) : (control f).run = f fun {β : Type u} (x : OptionT m β) => x.run

Option

instance instLawfulMonadOption : LawfulMonad Option

instance instLawfulApplicativeOption : LawfulApplicative Option

instance instLawfulFunctorOption : LawfulFunctor Option

ReaderT

theorem ReaderT.ext {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ReaderT ρ m α} (h : ∀ (ctx : ρ), x.run ctx = y.run ctx) : x = y

theorem ReaderT.ext_iff {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ReaderT ρ m α} : x = y ↔ ∀ (ctx : ρ), x.run ctx = y.run ctx

@[simp]

theorem ReaderT.run_mk {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (x : ρ → m α) (ctx : ρ) : (mk x).run ctx = x ctx

@[simp]

theorem ReaderT.run_pure {m : Type u_1 → Type u_2} {α ρ : Type u_1} [Monad m] (a : α) (ctx : ρ) : (pure a).run ctx = pure a

@[simp]

theorem ReaderT.run_bind {m : Type u_1 → Type u_2} {ρ α β : Type u_1} [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ) : (x >>= f).run ctx = do let a ← x.run ctx (f a).run ctx

@[simp]

theorem ReaderT.run_mapConst {m : Type u_1 → Type u_2} {α ρ β : Type u_1} [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ) : (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx)

@[simp]

theorem ReaderT.run_map {m : Type u_1 → Type u_2} {α β ρ : Type u_1} [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ) : (f <$> x).run ctx = f <$> x.run ctx

@[simp]

theorem ReaderT.run_monadLift {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {α ρ : Type u_1} [MonadLiftT n m] (x : n α) (ctx : ρ) : (monadLift x).run ctx = monadLift x

@[simp]

theorem ReaderT.run_monadMap {n : Type u → Type u_1} {m : Type u → Type u_2} {ρ α : Type u} [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ) : (monadMap f x).run ctx = monadMap f (x.run ctx)

@[simp]

theorem ReaderT.run_read {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] (ctx : ρ) : ReaderT.read.run ctx = pure ctx

@[simp]

theorem ReaderT.run_seq {m : Type u → Type u_1} {ρ α β : Type u} [Monad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ) : (f <*> x).run ctx = f.run ctx <*> x.run ctx

@[simp]

theorem ReaderT.run_seqRight {m : Type u_1 → Type u_2} {ρ α β : Type u_1} [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : (x *> y).run ctx = x.run ctx *> y.run ctx

@[simp]

theorem ReaderT.run_seqLeft {m : Type u_1 → Type u_2} {ρ α β : Type u_1} [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : (x <* y).run ctx = x.run ctx <* y.run ctx

instance ReaderT.instLawfulFunctor {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulFunctor m] : LawfulFunctor (ReaderT ρ m)

instance ReaderT.instLawfulApplicative {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulApplicative m] : LawfulApplicative (ReaderT ρ m)

instance ReaderT.instLawfulMonad {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m)

Note that the MonadControl instance for ReaderT is not monad-generic.

@[simp]

theorem ReaderT.run_restoreM {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Monad m] (x : stM m (ReaderT ρ m) α) (ctx : ρ) : (restoreM x).run ctx = pure x

@[simp]

theorem ReaderT.run_liftWith {m : Type u → Type u_1} {ρ α : Type u} [Monad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m α) (ctx : ρ) : (liftWith f).run ctx = f fun {β : Type u} (x : ReaderT ρ m β) => x.run ctx

@[simp]

theorem ReaderT.run_controlAt {m : Type u → Type u_1} {ρ α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) : (controlAt m f).run ctx = f fun {β : Type u} (x : ReaderT ρ m β) => x.run ctx

@[simp]

theorem ReaderT.run_control {m : Type u → Type u_1} {ρ α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) : (control f).run ctx = f fun {β : Type u} (x : ReaderT ρ m β) => x.run ctx

StateRefT

instance instLawfulMonadStateRefT' {m : Type → Type} {ω σ : Type} [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m)

StateT

theorem StateT.ext {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : StateT σ m α} (h : ∀ (s : σ), x.run s = y.run s) : x = y

theorem StateT.ext_iff {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : StateT σ m α} : x = y ↔ ∀ (s : σ), x.run s = y.run s

@[simp]

theorem StateT.run_mk {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] (x : σ → m (α × σ)) (s : σ) : (mk x).run s = x s

@[simp]

theorem StateT.run'_eq {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] (x : StateT σ m α) (s : σ) : x.run' s = (fun (x : α × σ) => x.fst) <$> x.run s

@[simp]

theorem StateT.run_pure {m : Type u_1 → Type u_2} {α σ : Type u_1} [Monad m] (a : α) (s : σ) : (pure a).run s = pure (a, s)

@[simp]

theorem StateT.run_bind {m : Type u_1 → Type u_2} {σ α β : Type u_1} [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ) : (x >>= f).run s = do let p ← x.run s (f p.fst).run p.snd

@[simp]

theorem StateT.run_map {m : Type u → Type u_1} {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.fst, p.snd)) <$> x.run s

@[simp]

theorem StateT.run_get {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (s : σ) : get.run s = pure (s, s)

@[simp]

theorem StateT.run_set {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (s s' : σ) : (set s').run s = pure (PUnit.unit, s')

@[simp]

theorem StateT.run_modify {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (f : σ → σ) (s : σ) : (modify f).run s = pure (PUnit.unit, f s)

@[simp]

theorem StateT.run_modifyGet {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f).run s = pure ((f s).fst, (f s).snd)

@[simp]

theorem StateT.run_lift {m : Type u → Type u_1} {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x).run s = do let a ← x pure (a, s)

theorem StateT.run_bind_lift {m : Type u → Type u_1} {β α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = do let a ← x (f a).run s

@[simp]

theorem StateT.run_monadLift {m : Type u → Type u_1} {n : Type u → Type u_2} {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x).run s = do let a ← monadLift x pure (a, s)

@[simp]

theorem StateT.run_monadMap {n : Type u → Type u_1} {m : Type u → Type u_2} {σ α : Type u} [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) : (monadMap f x).run s = monadMap f (x.run s)

@[simp]

theorem StateT.run_seq {m : Type u → Type u_1} {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = do let fs ← f.run s (fun (p : α × σ) => (fs.fst p.fst, p.snd)) <$> x.run fs.snd

@[simp]

theorem StateT.run_seqRight {m : Type u_1 → Type u_2} {σ α β : Type u_1} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = do let p ← x.run s y.run p.snd

@[simp]

theorem StateT.run_seqLeft {m : Type u → Type u_1} {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = do let p ← x.run s let p' ← y.run p.snd pure (p.fst, p'.snd)

theorem StateT.seqRight_eq {m : Type u_1 → Type u_2} {σ α β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = Function.const α id <$> x <*> y

theorem StateT.seqLeft_eq {m : Type u_1 → Type u_2} {σ α β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = Function.const β <$> x <*> y

instance StateT.instLawfulMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m)

Note that the MonadControl instance for StateT is not monad-generic.

@[simp]

theorem StateT.run_restoreM {m : Type u_1 → Type u_2} {σ α : Type u_1} [Monad m] [LawfulMonad m] (x : stM m (StateT σ m) α) (s : σ) : (restoreM x).run s = pure x

@[simp]

theorem StateT.run_liftWith {m : Type u → Type u_1} {σ α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m α) (s : σ) : (liftWith f).run s = (fun (x : α) => (x, s)) <$> f fun {β : Type u} (x : StateT σ m β) => x.run s

@[simp]

theorem StateT.run_controlAt {m : Type u → Type u_1} {σ α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) : (controlAt m f).run s = f fun {β : Type u} (x : StateT σ m β) => x.run s

@[simp]

theorem StateT.run_control {m : Type u → Type u_1} {σ α : Type u} [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) : (control f).run s = f fun {β : Type u} (x : StateT σ m β) => x.run s

EStateM

@[simp]

theorem EStateM.run_pure {α σ ε : Type u_1} (a : α) (s : σ) : (pure a).run s = Result.ok a s

@[simp]

theorem EStateM.run_get {σ ε : Type u_1} (s : σ) : get.run s = Result.ok s s

@[simp]

theorem EStateM.run_set {σ ε : Type u_1} (s₁ s₂ : σ) : (set s₁).run s₂ = Result.ok PUnit.unit s₁

@[simp]

theorem EStateM.run_modify {σ ε : Type u_1} (f : σ → σ) (s : σ) : (modify f).run s = Result.ok PUnit.unit (f s)

@[simp]

theorem EStateM.run_modifyGet {σ α ε : Type u_1} (f : σ → α × σ) (s : σ) : (modifyGet f).run s = Result.ok (f s).fst (f s).snd

@[simp]

theorem EStateM.run_throw {ε σ : Type u_1} (e : ε) (s : σ) : (throw e).run s = Result.error e s

@[simp]

theorem EStateM.run_bind {ε σ α β : Type u_1} {s : σ} (x : EStateM ε σ α) (f : α → EStateM ε σ β) : (x >>= f).run s = match x.run s with | Result.ok x s => (f x).run s | Result.error e s => Result.error e s

@[simp]

theorem EStateM.run_adaptExcept {ε ε' σ α : Type u_1} (f : ε → ε') (x : EStateM ε σ α) (s : σ) : (adaptExcept f x).run s = match x.run s with | Result.ok x s => Result.ok x s | Result.error e s => Result.error (f e) s

instance EStateM.instLawfulMonad {ε σ : Type u_1} : LawfulMonad (EStateM ε σ)