Functor Laws, applicative laws, and monad Laws

def StateT.mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) : StateT σ m α

Equations

• StateT.mk f = f

@[simp]

theorem StateT.run_mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) (st : σ) : (StateT.mk f).run st = f st

@[simp]

theorem ExceptT.run_monadLift {α ε : Type u} {m : Type u → Type v} {n : Type u → Type u_1} [Monad m] [MonadLiftT n m] (x : n α) : (monadLift x).run = Except.ok <$> monadLift x

@[simp]

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

def ReaderT.mk {m : Type u → Type v} {α σ : Type u} (f : σ → m α) : ReaderT σ m α

Equations

• ReaderT.mk f = f

@[simp]

theorem ReaderT.run_mk {m : Type u → Type v} {α σ : Type u} (f : σ → m α) (r : σ) : (ReaderT.mk f).run r = f r

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

@[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 {α : Type u} {m : Type u → Type v} [Monad m] (a : α) : (pure a).run = pure (some a)

@[simp]

theorem OptionT.run_bind {α β : Type u} {m : Type u → Type v} (x : OptionT m α) [Monad m] (f : α → OptionT m β) : (x >>= f).run = do let x ← x.run match x with | some a => (f a).run | none => pure none

@[simp]

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

@[simp]

theorem OptionT.run_monadLift {α : Type u} {m : Type u → Type v} [Monad m] {n : Type u → Type u_1} [MonadLiftT n m] (x : n α) : (monadLift x).run = do let a ← monadLift x pure (some a)

@[simp]

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

instance instLawfulMonadOptionT_mathlib (m : Type u → Type v) [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m)