# Documentation

## Init.Control.Lawful

@[simp]
theorem monadLift_self {m : Type u_1 → Type u_2} {α : Type u_1} [] (x : m α) :
= x
class LawfulFunctor (f : Type u → Type v) [] :
• map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map
• id_map : ∀ {α : Type u} (x : f α), id <$> x = x • comp_map : ∀ {α β γ : Type u} (g : αβ) (h : βγ) (x : f α), (h g) <$> x = h <$> g <$> x
Instances
@[simp]
theorem id_map' {m : Type u_1 → Type u_2} {α : Type u_1} [] [] (x : m α) :
(fun (a : α) => a) <$> x = x class LawfulApplicative (f : Type u → Type v) [] extends : Instances @[simp] theorem pure_id_seq {f : Type u_1 → Type u_2} {α : Type u_1} [] (x : f α) : (Seq.seq (pure id) fun (x_1 : Unit) => x) = x class LawfulMonad (m : Type u → Type v) [] extends : • map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map • id_map : ∀ {α : Type u} (x : m α), id <$> x = x
• comp_map : ∀ {α β γ : Type u} (g : αβ) (h : βγ) (x : m α), (h g) <$> x = h <$> g <$> x • seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq () fun (x : Unit) => y • seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq ( <$> x) fun (x : Unit) => y
• pure_seq : ∀ {α β : Type u} (g : αβ) (x : m α), (Seq.seq (pure g) fun (x_1 : Unit) => x) = g <$> x • map_pure : ∀ {α β : Type u} (g : αβ) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : m (αβ)) (x : α), (Seq.seq g fun (x_1 : Unit) => pure x) = (fun (h : αβ) => h x) <$> g • seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (αβ)) (h : m (βγ)), (Seq.seq h fun (x_1 : Unit) => Seq.seq g fun (x_2 : Unit) => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun (x : Unit) => g) fun (x_1 : Unit) => x
• 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 x_1 ← f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => 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
@[simp]
theorem bind_pure {m : Type u_1 → Type u_2} {α : Type u_1} [] [] (x : m α) :
x >>= pure = x
theorem map_eq_pure_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] [] (f : αβ) (x : m α) :
f <$> x = do let a ← x pure (f a) theorem seq_eq_bind_map {m : Type u → Type u_1} {α : Type u} {β : Type u} [] [] (f : m (αβ)) (x : m α) : (Seq.seq f fun (x_1 : Unit) => x) = do let x_1 ← f x_1 <$> x
theorem bind_congr {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Bind m] {x : m α} {f : αm β} {g : αm β} (h : ∀ (a : α), f a = g a) :
x >>= f = x >>= g
@[simp]
theorem bind_pure_unit {m : Type u_1 → Type u_2} [] [] {x : } :
(do x ) = x
theorem map_congr {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] {x : m α} {f : αβ} {g : αβ} (h : ∀ (a : α), f a = g a) :
f <$> x = g <$> x
theorem seq_eq_bind {m : Type u → Type u_1} {α : Type u} {β : Type u} [] [] (mf : m (αβ)) (x : m α) :
(Seq.seq mf fun (x_1 : Unit) => x) = do let f ← mf f <$> x theorem seqRight_eq_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] [] (x : m α) (y : m β) : (SeqRight.seqRight x fun (x : Unit) => y) = do let _ ← x y theorem seqLeft_eq_bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] [] (x : m α) (y : m β) : (SeqLeft.seqLeft x fun (x : Unit) => y) = do let a ← x let _ ← y pure a theorem LawfulMonad.mk' (m : Type u → Type v) [] (id_map : ∀ {α : Type u} (x : m α), id <$> x = 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) (map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), = <$> y) _auto✝) (seqLeft_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun (x : Unit) => y) = do let a ← x let _ ← y pure a) _auto✝) (seqRight_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = do let _ ← x y) _auto✝) (bind_pure_comp : autoParam (∀ {α β : Type u} (f : αβ) (x : m α), (do let y ← x pure (f y)) = f <$> x) _auto✝) (bind_map : autoParam (∀ {α β : Type u} (f : m (αβ)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => x) _auto✝) : An alternative constructor for LawfulMonad which has more defaultable fields in the common case. # Id # @[simp] theorem Id.map_eq {α : Type u_1} {β : Type u_1} (x : Id α) (f : αβ) : f <$> x = f x
@[simp]
theorem Id.bind_eq {α : Type u_1} {β : Type u_1} (x : Id α) (f : αid β) :
x >>= f = f x
@[simp]
theorem Id.pure_eq {α : Type u_1} (a : α) :
pure a = a
Equations

# ExceptT #

theorem ExceptT.ext {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [] {x : ExceptT ε m α} {y : ExceptT ε m α} (h : ) :
x = y
@[simp]
theorem ExceptT.run_pure {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} [] (x : α) :
@[simp]
theorem ExceptT.run_lift {m : Type u → Type v} {α : Type u} {ε : Type u} [] (x : m α) :
= Except.ok <$> x @[simp] theorem ExceptT.run_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {β : Type u_1} {e : ε} [] : @[simp] theorem ExceptT.run_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} [] [] (x : m α) (f : αExceptT ε m β) : ExceptT.run () = 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 : ε} [] [] (f : αExceptT ε m β) : >>= f = theorem ExceptT.run_bind {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} {f : αExceptT ε m β} [] (x : ExceptT ε m α) : ExceptT.run (x >>= f) = do let x ← match x with | => ExceptT.run (f x) | => pure () @[simp] theorem ExceptT.lift_pure {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} [] [] (a : α) : @[simp] theorem ExceptT.run_map {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ε : Type u_1} [] [] (f : αβ) (x : ExceptT ε m α) : theorem ExceptT.seq_eq {m : Type u → Type u_1} {α : Type u} {β : Type u} {ε : Type u} [] (mf : ExceptT ε m (αβ)) (x : ExceptT ε m α) : (Seq.seq mf fun (x_1 : Unit) => x) = do let f ← mf f <$> x
theorem ExceptT.bind_pure_comp {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ε : Type u_1} [] [] (f : αβ) (x : ExceptT ε m α) :
x >>= pure f = f <$> x theorem ExceptT.seqLeft_eq {α : Type u} {β : Type u} {ε : Type u} {m : Type u → Type v} [] [] (x : ExceptT ε m α) (y : ExceptT ε m β) : (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq () fun (x : Unit) => y theorem ExceptT.seqRight_eq {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} [] [] (x : ExceptT ε m α) (y : ExceptT ε m β) : (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq ( <$> x) fun (x : Unit) => y
instance ExceptT.instLawfulMonadExceptTInstMonadExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} [] [] :
Equations
• =

# Except #

Equations
• =

theorem ReaderT.ext {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {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} [] (a : α) (ctx : ρ) :
@[simp]
theorem ReaderT.run_bind {m : Type u_1 → Type u_2} {ρ : Type u_1} {α : Type u_1} {β : Type u_1} [] (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_mapConst {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_1} {β : Type u_1} [] (a : α) (x : ReaderT ρ m β) (ctx : ρ) :
@[simp]
theorem ReaderT.run_map {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {ρ : Type u_1} [] (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} [] (x : n α) (ctx : ρ) :
@[simp]
theorem ReaderT.run_monadMap {n : Type u → Type u_1} {m : Type u → Type u_2} {ρ : Type u} {α : Type u} [] (f : {β : Type u} → n βn β) (x : ReaderT ρ m α) (ctx : ρ) :
@[simp]
theorem ReaderT.run_read {m : Type u_1 → Type u_2} {ρ : Type u_1} [] (ctx : ρ) :
@[simp]
theorem ReaderT.run_seq {m : Type u → Type u_1} {ρ : Type u} {α : Type u} {β : Type u} [] (f : ReaderT ρ m (αβ)) (x : ReaderT ρ m α) (ctx : ρ) :
ReaderT.run (Seq.seq f fun (x_1 : Unit) => x) ctx = Seq.seq (ReaderT.run f ctx) fun (x_1 : Unit) => 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} [] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) :
ReaderT.run (SeqRight.seqRight x fun (x : Unit) => y) ctx = SeqRight.seqRight (ReaderT.run x ctx) fun (x : Unit) => 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} [] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) :
ReaderT.run (SeqLeft.seqLeft x fun (x : Unit) => y) ctx = SeqLeft.seqLeft (ReaderT.run x ctx) fun (x : Unit) => ReaderT.run y ctx
Equations
• =
Equations
• =
Equations
• =

# StateRefT #

instance instLawfulMonadStateRefT'InstMonadStateRefT' {m : } {ω : Type} {σ : Type} [] [] :
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 = y
@[simp]
theorem StateT.run'_eq {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [] (x : StateT σ m α) (s : σ) :
= (fun (x : α × σ) => x.fst) <$> @[simp] theorem StateT.run_pure {m : Type u_1 → Type u_2} {α : Type u_1} {σ : Type u_1} [] (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} [] (x : StateT σ m α) (f : αStateT σ m β) (s : σ) : StateT.run (x >>= f) s = do let p ← StateT.run (f p.fst) p.snd @[simp] theorem StateT.run_map {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [] [] (f : αβ) (x : StateT σ m α) (s : σ) : StateT.run (f <$> x) s = (fun (p : α × σ) => (f p.fst, p.snd)) <$> @[simp] theorem StateT.run_get {m : Type u_1 → Type u_2} {σ : Type u_1} [] (s : σ) : StateT.run get s = pure (s, s) @[simp] theorem StateT.run_set {m : Type u_1 → Type u_2} {σ : Type u_1} [] (s : σ) (s' : σ) : @[simp] theorem StateT.run_modify {m : Type u_1 → Type u_2} {σ : Type u_1} [] (f : σσ) (s : σ) : @[simp] theorem StateT.run_modifyGet {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_1} [] (f : σα × σ) (s : σ) : StateT.run () s = pure ((f s).fst, (f s).snd) @[simp] theorem StateT.run_lift {m : Type u → Type u_1} {α : Type u} {σ : Type u} [] (x : m α) (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} [] [] (x : m α) (f : αStateT σ m β) (s : σ) : StateT.run () 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} [] [] (x : n α) (s : σ) : StateT.run () s = do let a ← pure (a, s) @[simp] theorem StateT.run_monadMap {m : Type u → Type u_1} {n : Type u → Type u_2} {σ : Type u} {α : Type u} [] [] (f : {β : Type u} → n βn β) (x : StateT σ m α) (s : σ) : @[simp] theorem StateT.run_seq {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [] [] (f : StateT σ m (αβ)) (x : StateT σ m α) (s : σ) : StateT.run (Seq.seq f fun (x_1 : Unit) => x) s = do let fs ← (fun (p : α × σ) => (fs.fst 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} [] [] (x : StateT σ m α) (y : StateT σ m β) (s : σ) :
StateT.run (SeqRight.seqRight x fun (x : Unit) => y) s = do let p ← StateT.run y p.snd
@[simp]
theorem StateT.run_seqLeft {m : Type u → Type u_1} {α : Type u} {β : Type u} {σ : Type u} [] [] (x : StateT σ m α) (y : StateT σ m β) (s : σ) :
StateT.run (SeqLeft.seqLeft x fun (x : Unit) => y) s = do let p ← 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} [] [] (x : StateT σ m α) (y : StateT σ m β) :
(SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq ( <\$> 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} [] [] (x : StateT σ m α) (y : StateT σ m β) :
(SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq () fun (x : Unit) => y
instance StateT.instLawfulMonadStateTInstMonadStateT {m : Type u_1 → Type u_2} {σ : Type u_1} [] [] :
Equations
• =