Documentation

Init.Control.Lawful.Instances

ExceptT #

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
@[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)
@[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
@[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)
@[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 ax (f a).run
@[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 β) :
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 xx.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} {ε : Type u_1} [Monad m] [LawfulMonad m] (a : α) :
@[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
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 fmf f <$> x
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
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
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
instance ExceptT.instLawfulMonad {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] :
Equations
  • =
@[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 : ε) :

Except #

instance instLawfulMonadExcept {ε : Type u_1} :
Equations
  • =
Equations
  • =
Equations
  • =

ReaderT #

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
@[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
@[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 ax.run ctx (f a).run ctx
@[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)
@[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
@[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
@[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)
@[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} {α : 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
@[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
@[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
instance ReaderT.instLawfulFunctor {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulFunctor m] :
Equations
  • =
instance ReaderT.instLawfulApplicative {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulApplicative m] :
Equations
  • =
instance ReaderT.instLawfulMonad {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulMonad m] :
Equations
  • =

StateRefT #

instance instLawfulMonadStateRefT' {m : TypeType} {ω : Type} {σ : Type} [Monad m] [LawfulMonad m] :
Equations
  • =

StateT #

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
@[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
@[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)
@[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 px.run s (f p.fst).run p.snd
@[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
@[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} {α : 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} {σ : Type u} [Monad m] (x : m α) (s : σ) :
(StateT.lift x).run s = do let ax pure (a, s)
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 ax (f a).run s
@[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 amonadLift x pure (a, s)
@[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)
@[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 fsf.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} {α : 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 px.run s y.run p.snd
@[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 px.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} {α : 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
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 β) :
(SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq (Function.const β <$> x) fun (x : Unit) => y
instance StateT.instLawfulMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] [LawfulMonad m] :
Equations
  • =

EStateM #

instance instLawfulMonadEStateM {ε : Type u_1} {σ : Type u_1} :
Equations
  • =