ExceptT #

source

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

x = y

source

@[simp]

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

(pure x).run = pure (Except.ok x)

source

@[simp]

theorem ExceptT.run_lift {m : Type u → Type v} {α : Type u} {ε : Type u} [Monad m] (x : m α) :

(ExceptT.lift x).run = Except.ok <$> x

source

@[simp]

theorem ExceptT.run_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {β : Type u_1} {e : ε} [Monad m] :

(throw e).run = pure (Except.error e)

source

@[simp]

theorem ExceptT.run_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) :

(ExceptT.lift x >>= f).run = do let a ← x (f a).run

source

@[simp]

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

throw e >>= f = throw e

source

theorem ExceptT.run_bind {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} {f : α → ExceptT ε m β} [Monad m] (x : 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)

source

@[simp]

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

ExceptT.lift (pure a) = pure a

source

@[simp]

theorem ExceptT.run_map {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) :

(f <$> x).run = Except.map f <$> x.run

source

theorem ExceptT.seq_eq {m : Type u → Type u_1} {α : Type u} {β : Type u} {ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) :

(Seq.seq mf fun (x_1 : Unit) => x) = do let f ← mf f <$> x

source

theorem ExceptT.bind_pure_comp {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ε : Type u_1} [Monad m] (f : α → β) (x : ExceptT ε m α) :

x >>= pure ∘ f = f <$> x

source

theorem ExceptT.seqLeft_eq {α : Type u} {β : Type u} {ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) :

(SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq (Function.const β <$> x) fun (x : Unit) => y

source

theorem ExceptT.seqRight_eq {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) :

(SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq (Function.const α id <$> x) fun (x : Unit) => y

source

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

LawfulMonad (ExceptT ε m)

Equations

⋯ = ⋯

source

@[simp]

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

f <$> throw e = throw e

Except #

source

instance instLawfulMonadExcept {ε : Type u_1} :

LawfulMonad (Except ε)

Equations

⋯ = ⋯

source

instance instLawfulApplicativeExcept {ε : Type u_1} :

LawfulApplicative (Except ε)

Equations

⋯ = ⋯

source

instance instLawfulFunctorExcept {ε : Type u_1} :

LawfulFunctor (Except ε)

Equations

⋯ = ⋯

ReaderT #

source

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

x = y

source

@[simp]

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

(pure a).run ctx = pure a

source

@[simp]

theorem ReaderT.run_bind {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} {β : 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

source

@[simp]

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

(Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx)

source

@[simp]

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

(f <$> x).run ctx = f <$> x.run ctx

source

@[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} [MonadLiftT n m] (x : n α) (ctx : ρ) :

(monadLift x).run ctx = monadLift x

source

@[simp]

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

(monadMap f x).run ctx = monadMap f (x.run ctx)

source

@[simp]

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

ReaderT.read.run ctx = pure ctx

source

@[simp]

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

(Seq.seq f fun (x_1 : Unit) => x).run ctx = Seq.seq (f.run ctx) fun (x_1 : Unit) => x.run ctx

source

@[simp]

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

(SeqRight.seqRight x fun (x : Unit) => y).run ctx = SeqRight.seqRight (x.run ctx) fun (x : Unit) => y.run ctx

source

@[simp]

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

(SeqLeft.seqLeft x fun (x : Unit) => y).run ctx = SeqLeft.seqLeft (x.run ctx) fun (x : Unit) => y.run ctx

source

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

LawfulFunctor (ReaderT ρ m)

Equations

⋯ = ⋯

source

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

LawfulApplicative (ReaderT ρ m)

Equations

⋯ = ⋯

source

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

LawfulMonad (ReaderT ρ m)

Equations

⋯ = ⋯

StateRefT #

source

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

LawfulMonad (StateRefT' ω σ m)

Equations

⋯ = ⋯

StateT #

source

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

x = y

source

@[simp]

theorem StateT.run'_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [Monad m] (x : StateT σ m α) (s : σ) :

x.run' s = (fun (x : α × σ) => x.fst) <$> x.run s

source

@[simp]

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

(pure a).run s = pure (a, s)

source

@[simp]

theorem StateT.run_bind {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : 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

source

@[simp]

theorem StateT.run_map {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : 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

source

@[simp]

theorem StateT.run_get {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (s : σ) :

get.run s = pure (s, s)

source

@[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')

source

@[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)

source

@[simp]

theorem StateT.run_modifyGet {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [Monad m] (f : σ → α × σ) (s : σ) :

(modifyGet f).run s = pure ((f s).fst, (f s).snd)

source

@[simp]

theorem StateT.run_lift {m : Type u → Type u_1} {α : Type u} {σ : Type u} [Monad m] (x : m α) (s : σ) :

(StateT.lift x).run s = do let a ← x pure (a, s)

source

theorem StateT.run_bind_lift {m : Type u → Type u_1} {β : Type u} {α : Type u} {σ : 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

source

@[simp]

theorem StateT.run_monadLift {m : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u} {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) :

(monadLift x).run s = do let a ← monadLift x pure (a, s)

source

@[simp]

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

(monadMap f x).run s = monadMap f (x.run s)

source

@[simp]

theorem StateT.run_seq {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) :

(Seq.seq f fun (x_1 : Unit) => x).run s = do let fs ← f.run s (fun (p : α × σ) => (fs.fst p.fst, p.snd)) <$> x.run fs.snd

source

@[simp]

theorem StateT.run_seqRight {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) :

(SeqRight.seqRight x fun (x : Unit) => y).run s = do let p ← x.run s y.run p.snd

source

@[simp]

theorem StateT.run_seqLeft {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) :

(SeqLeft.seqLeft x fun (x : Unit) => y).run s = do let p ← x.run s let p' ← y.run p.snd pure (p.fst, p'.snd)

source

theorem StateT.seqRight_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) :

(SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq (Function.const α id <$> x) fun (x : Unit) => y

source

theorem StateT.seqLeft_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) :