@[simp]
- seqLeft_eq : ∀ {α β : Type u} (x : f α) (y : f β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
- seqRight_eq : ∀ {α β : Type u} (x : f α) (y : f β), (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
- pure_seq : ∀ {α β : Type u} (g : α → β) (x : f α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
- map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
- seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
- seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
Instances
@[simp]
theorem
pure_id_seq
{f : Type u_1 → Type u_2}
{α : Type u_1}
[inst : Applicative f]
[inst : LawfulApplicative f]
(x : f α)
:
- bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α), (do let a ← x pure (f a)) = f <$> x
- bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α), (do let a ← f a <$> x) = Seq.seq f fun x_1 => x
- pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
- bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
Instances
- ExceptCpsT.instLawfulMonadExceptCpsTInstMonadExceptCpsT
- ExceptT.instLawfulMonadExceptTInstMonadExceptT
- Id.instLawfulMonadIdInstMonadId
- instLawfulMonadStateRefT'InstMonadStateRefT'
- StateT.instLawfulMonadStateTInstMonadStateT
- StateCpsT.instLawfulMonadStateCpsTInstMonadStateCpsT
- ReaderT.instLawfulMonadReaderTInstMonadReaderT
theorem
map_eq_pure_bind
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(f : α → β)
(x : m α)
:
theorem
seq_eq_bind_map
{m : Type u → Type u_1}
{α : Type u}
{β : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(f : m (α → β))
(x : m α)
:
@[simp]
theorem
bind_pure_unit
{m : Type u_1 → Type u_2}
[inst : Monad m]
[inst : LawfulMonad m]
{x : m PUnit}
:
(do
x
pure PUnit.unit) = x
theorem
seq_eq_bind
{m : Type u → Type u_1}
{α : Type u}
{β : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(mf : m (α → β))
(x : m α)
:
theorem
seqRight_eq_bind
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : m α)
(y : m β)
:
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y
theorem
seqLeft_eq_bind
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : m α)
(y : m β)
:
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a
theorem
ExceptT.ext
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{α : Type u_1}
[inst : Monad m]
{x : ExceptT ε m α}
{y : ExceptT ε m α}
(h : ExceptT.run x = ExceptT.run y)
:
x = y
@[simp]
theorem
ExceptT.run_pure
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{α : Type u_1}
{x : α}
[inst : Monad m]
:
ExceptT.run (pure x) = pure (Except.ok x)
@[simp]
theorem
ExceptT.run_lift
{m : Type (max u_1 u_2) → Type u_3}
{α : Type (max u_1 u_2)}
{ε : Type (max u_1 u_2)}
[inst : Monad m]
(x : m α)
:
ExceptT.run (ExceptT.lift x) = Except.ok <$> x
@[simp]
theorem
ExceptT.run_throw
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{β : Type u_1}
{e : ε}
[inst : Monad m]
:
ExceptT.run (throw e) = pure (Except.error e)
@[simp]
theorem
ExceptT.run_bind_lift
{m : Type u_1 → Type u_2}
{α : Type u_1}
{ε : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : m α)
(f : α → ExceptT ε m β)
:
ExceptT.run (ExceptT.lift x >>= f) = do
let a ← x
ExceptT.run (f a)
@[simp]
theorem
ExceptT.bind_throw
{m : Type u_1 → Type u_2}
{α : Type u_1}
{ε : Type u_1}
{β : Type u_1}
{e : ε}
[inst : Monad m]
[inst : LawfulMonad m]
(f : α → ExceptT ε m β)
:
theorem
ExceptT.run_bind
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{α : Type u_1}
{β : Type u_1}
{f : α → ExceptT ε m β}
[inst : Monad m]
(x : ExceptT ε m α)
:
ExceptT.run (x >>= f) = do
let x ← ExceptT.run x
match x with
| Except.ok x => ExceptT.run (f x)
| Except.error e => pure (Except.error e)
@[simp]
theorem
ExceptT.lift_pure
{m : Type u_1 → Type u_2}
{α : Type u_1}
{ε : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(a : α)
:
ExceptT.lift (pure a) = pure a
@[simp]
theorem
ExceptT.run_map
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
{ε : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(f : α → β)
(x : ExceptT ε m α)
:
ExceptT.run (f <$> x) = Except.map f <$> ExceptT.run x
theorem
ExceptT.bind_pure_comp
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
{ε : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(f : α → β)
(x : ExceptT ε m α)
:
theorem
ExceptT.seqLeft_eq
{α : Type u}
{β : Type u}
{ε : Type u}
{m : Type u → Type v}
[inst : Monad m]
[inst : LawfulMonad m]
(x : ExceptT ε m α)
(y : ExceptT ε m β)
:
(SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
theorem
ExceptT.seqRight_eq
{m : Type u_1 → Type u_2}
{ε : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : ExceptT ε m α)
(y : ExceptT ε m β)
:
(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
noncomputable instance
ExceptT.instLawfulMonadExceptTInstMonadExceptT
{m : Type u_1 → Type u_2}
{ε : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
:
LawfulMonad (ExceptT ε m)
theorem
ReaderT.ext
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
[inst : Monad m]
{x : ReaderT ρ m α}
{y : ReaderT ρ m α}
(h : ∀ (ctx : ρ), ReaderT.run x ctx = ReaderT.run y ctx)
:
x = y
@[simp]
theorem
ReaderT.run_pure
{m : Type u_1 → Type u_2}
{α : Type u_1}
{ρ : Type u_1}
[inst : Monad m]
(a : α)
(ctx : ρ)
:
ReaderT.run (pure a) ctx = pure a
@[simp]
theorem
ReaderT.run_bind
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
(x : ReaderT ρ m α)
(f : α → ReaderT ρ m β)
(ctx : ρ)
:
ReaderT.run (x >>= f) ctx = do
let a ← ReaderT.run x ctx
ReaderT.run (f a) ctx
@[simp]
theorem
ReaderT.run_map
{m : Type u_1 → Type u_2}
{α : Type u_1}
{β : Type u_1}
{ρ : Type u_1}
[inst : Monad m]
(f : α → β)
(x : ReaderT ρ m α)
(ctx : ρ)
:
ReaderT.run (f <$> x) ctx = f <$> ReaderT.run x ctx
@[simp]
theorem
ReaderT.run_monadLift
{n : Type u_1 → Type u_2}
{m : Type u_1 → Type u_3}
{α : Type u_1}
{ρ : Type u_1}
[inst : MonadLiftT n m]
(x : n α)
(ctx : ρ)
:
ReaderT.run (monadLift x) ctx = monadLift x
@[simp]
theorem
ReaderT.run_monadMap
{m : Type u → Type u_1}
{n : Type u → Type u_2}
{ρ : Type u}
{α : Type u}
[inst : Monad m]
[inst : MonadFunctor n m]
(f : {β : Type u} → n β → n β)
(x : ReaderT ρ m α)
(ctx : ρ)
:
ReaderT.run (monadMap f x) ctx = monadMap f (ReaderT.run x ctx)
@[simp]
theorem
ReaderT.run_read
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
[inst : Monad m]
(ctx : ρ)
:
ReaderT.run ReaderT.read ctx = pure ctx
@[simp]
theorem
ReaderT.run_seq
{m : Type u → Type u_1}
{ρ : Type u}
{α : Type u}
{β : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(f : ReaderT ρ m (α → β))
(x : ReaderT ρ m α)
(ctx : ρ)
:
ReaderT.run (Seq.seq f fun x => x) ctx = Seq.seq (ReaderT.run f ctx) fun x => ReaderT.run x ctx
@[simp]
theorem
ReaderT.run_seqRight
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : ReaderT ρ m α)
(y : ReaderT ρ m β)
(ctx : ρ)
:
ReaderT.run (SeqRight.seqRight x fun x => y) ctx = SeqRight.seqRight (ReaderT.run x ctx) fun x => ReaderT.run y ctx
@[simp]
theorem
ReaderT.run_seqLeft
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : ReaderT ρ m α)
(y : ReaderT ρ m β)
(ctx : ρ)
:
ReaderT.run (SeqLeft.seqLeft x fun x => y) ctx = SeqLeft.seqLeft (ReaderT.run x ctx) fun x => ReaderT.run y ctx
noncomputable instance
ReaderT.instLawfulMonadReaderTInstMonadReaderT
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
:
LawfulMonad (ReaderT ρ m)
noncomputable instance
instLawfulMonadStateRefT'InstMonadStateRefT'
{m : Type → Type}
{ω : Type}
{σ : Type}
[inst : Monad m]
[inst : LawfulMonad m]
:
LawfulMonad (StateRefT' ω σ m)
theorem
StateT.ext
{σ : Type u_1}
{m : Type u_1 → Type u_2}
{α : Type u_1}
{x : StateT σ m α}
{y : StateT σ m α}
(h : ∀ (s : σ), StateT.run x s = StateT.run y s)
:
x = y
@[simp]
theorem
StateT.run'_eq
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
[inst : Monad m]
(x : StateT σ m α)
(s : σ)
:
StateT.run' x s = (fun a => a.fst) <$> StateT.run x s
@[simp]
theorem
StateT.run_pure
{m : Type u_1 → Type u_2}
{α : Type u_1}
{σ : Type u_1}
[inst : Monad m]
(a : α)
(s : σ)
:
StateT.run (pure a) s = pure (a, s)
@[simp]
theorem
StateT.run_bind
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
(x : StateT σ m α)
(f : α → StateT σ m β)
(s : σ)
:
StateT.run (x >>= f) s = do
let p ← StateT.run x s
StateT.run (f p.fst) p.snd
@[simp]
theorem
StateT.run_map
{m : Type u → Type u_1}
{α : Type u}
{β : Type u}
{σ : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(f : α → β)
(x : StateT σ m α)
(s : σ)
:
StateT.run (f <$> x) s = (fun p => (f p.fst, p.snd)) <$> StateT.run x s
@[simp]
theorem
StateT.run_get
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[inst : Monad m]
(s : σ)
:
StateT.run get s = pure (s, s)
@[simp]
theorem
StateT.run_set
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[inst : Monad m]
(s : σ)
(s' : σ)
:
StateT.run (set s') s = pure (PUnit.unit, s')
@[simp]
theorem
StateT.run_modify
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[inst : Monad m]
(f : σ → σ)
(s : σ)
:
StateT.run (modify f) s = pure (PUnit.unit, f s)
@[simp]
theorem
StateT.run_modifyGet
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
[inst : Monad m]
(f : σ → α × σ)
(s : σ)
:
StateT.run (modifyGet f) s = pure ((f s).fst, (f s).snd)
@[simp]
theorem
StateT.run_lift
{m : Type u → Type u_1}
{α : Type u}
{σ : Type u}
[inst : Monad m]
(x : m α)
(s : σ)
:
StateT.run (StateT.lift x) s = do
let a ← x
pure (a, s)
@[simp]
theorem
StateT.run_bind_lift
{m : Type u → Type u_1}
{β : Type u}
{α : Type u}
{σ : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(x : m α)
(f : α → StateT σ m β)
(s : σ)
:
StateT.run (StateT.lift x >>= f) s = do
let a ← x
StateT.run (f a) s
@[simp]
theorem
StateT.run_monadLift
{m : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{σ : Type u}
[inst : Monad m]
[inst : MonadLiftT n m]
(x : n α)
(s : σ)
:
StateT.run (monadLift x) s = do
let a ← monadLift x
pure (a, s)
@[simp]
theorem
StateT.run_monadMap
{m : Type u → Type u_1}
{n : Type u → Type u_2}
{σ : Type u}
{α : Type u}
[inst : Monad m]
[inst : MonadFunctor n m]
(f : {β : Type u} → n β → n β)
(x : StateT σ m α)
(s : σ)
:
StateT.run (monadMap f x) s = monadMap f (StateT.run x s)
@[simp]
theorem
StateT.run_seq
{m : Type u → Type u_1}
{α : Type u}
{β : Type u}
{σ : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(f : StateT σ m (α → β))
(x : StateT σ m α)
(s : σ)
:
StateT.run (Seq.seq f fun x => x) s = do
let fs ← StateT.run f s
(fun p => (Prod.fst (α → β) σ fs p.fst, p.snd)) <$> StateT.run x fs.snd
@[simp]
theorem
StateT.run_seqRight
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : StateT σ m α)
(y : StateT σ m β)
(s : σ)
:
StateT.run (SeqRight.seqRight x fun x => y) s = do
let p ← StateT.run x s
StateT.run y p.snd
@[simp]
theorem
StateT.run_seqLeft
{m : Type u → Type u_1}
{α : Type u}
{β : Type u}
{σ : Type u}
[inst : Monad m]
[inst : LawfulMonad m]
(x : StateT σ m α)
(y : StateT σ m β)
(s : σ)
:
StateT.run (SeqLeft.seqLeft x fun x => y) s = do
let p ← StateT.run x s
let p' ← StateT.run y p.snd
pure (p.fst, p'.snd)
theorem
StateT.seqRight_eq
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : StateT σ m α)
(y : StateT σ m β)
:
(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
theorem
StateT.seqLeft_eq
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{α : Type u_1}
{β : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
(x : StateT σ m α)
(y : StateT σ m β)
:
(SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
noncomputable instance
StateT.instLawfulMonadStateTInstMonadStateT
{m : Type u_1 → Type u_2}
{σ : Type u_1}
[inst : Monad m]
[inst : LawfulMonad m]
:
LawfulMonad (StateT σ m)