Lemmas About Option Monad Transformer

This file contains lemmas about the behavior of OptionT and OptionT.run.

@[simp]

theorem Option.elimM_pure {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α → m β) : elimM (pure x) y z = x.elim y z

@[simp]

theorem Option.elimM_bind {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → m (Option β)) (y : m γ) (z : β → m γ) : elimM (x >>= f) y z = do let __do_lift ← x elimM (f __do_lift) y z

@[simp]

theorem Option.elimM_map {m : Type u_1 → Type u_2} {α β γ : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → Option β) (y : m γ) (z : β → m γ) : elimM (f <$> x) y z = do let __do_lift ← x (f __do_lift).elim y z

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

@[simp]

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

@[simp]

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

@[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) (run ∘ f)

@[simp]

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

@[simp]

theorem OptionT.run_monadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadLiftT n m] (x : n α) : (monadLift x).run = some <$> monadLift x

@[simp]

theorem OptionT.run_mapConst {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : β) : (Functor.mapConst y x).run = Option.map (Function.const α y) <$> x.run

instance OptionT.instLawfulMonad_batteries (m : Type u_1 → Type u_2) [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m)

@[simp]

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

@[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 (pure ∘ some)

@[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_monadMap {m : Type u_1 → Type u_2} {α : Type u_1} {x : OptionT m α} {n : Type u_1 → Type u_3} [MonadFunctorT n m] (f : {α : Type u_1} → n α → n α) : (monadMap f x).run = monadMap f x.run