# Documentation

Mathlib.Control.Basic

Extends the theory on functors, applicatives and monads.

theorem Functor.map_map {α : Type u} {β : Type u} {γ : Type u} {f : Type u → Type v} [] [] (m : αβ) (g : βγ) (x : f α) :
g <$> m <$> x = (g m) <$> x def zipWithM {F : Type u → Type v} [] {α₁ : Type u} {α₂ : Type u} {φ : Type u} (f : α₁α₂F φ) : List α₁List α₂F (List φ) A generalization of List.zipWith which combines list elements with an Applicative. Equations Instances For def zipWithM' {α : Type u} {β : Type u} {γ : Type u} {F : Type u → Type v} [] (f : αβF γ) : List αList β Like zipWithM but evaluates the result as it traverses the lists using *>. Equations Instances For @[simp] theorem pure_id'_seq {α : Type u} {F : Type u → Type v} [] (x : F α) : (Seq.seq (pure fun x => x) fun x => x) = x theorem seq_map_assoc {α : Type u} {β : Type u} {γ : Type u} {F : Type u → Type v} [] (x : F (αβ)) (f : γα) (y : F γ) : (Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x f) <$> x) fun x => y theorem map_seq {α : Type u} {β : Type u} {γ : Type u} {F : Type u → Type v} [] (f : βγ) (x : F (αβ)) (y : F α) : (f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f x) <$> x) fun x => y theorem map_bind {α : Type u} {β : Type u} {γ : Type u} {m : Type u → Type v} [] [] (x : m α) {g : αm β} {f : βγ} : f <$> (x >>= g) = do let a ← x f <$> g a theorem seq_bind_eq {α : Type u} {β : Type u} {γ : Type u} {m : Type u → Type v} [] [] (x : m α) {g : βm γ} {f : αβ} : f <$> x >>= g = x >>= g f
theorem fish_pure {m : Type u → Type v} [] [] {α : Type u_1} {β : Type u} (f : αm β) :
f >=> pure = f
theorem fish_pipe {m : Type u → Type v} [] [] {α : Type u} {β : Type u} (f : αm β) :
pure >=> f = f
theorem fish_assoc {m : Type u → Type v} [] [] {α : Type u_1} {β : Type u} {γ : Type u} {φ : Type u} (f : αm β) (g : βm γ) (h : γm φ) :
(f >=> g) >=> h = f >=> g >=> h
def List.mapAccumRM {α : Type u} {β' : Type v} {γ' : Type v} {m' : Type v → Type w} [Monad m'] (f : αβ'm' (β' × γ')) :
β'List αm' (β' × List γ')

Takes a value β and List α and accumulates pairs according to a monadic function f. Accumulation occurs from the right (i.e., starting from the tail of the list).

Equations
Instances For
def List.mapAccumLM {α : Type u} {β' : Type v} {γ' : Type v} {m' : Type v → Type w} [Monad m'] (f : β'αm' (β' × γ')) :
β'List αm' (β' × List γ')

Takes a value β and List α and accumulates pairs according to a monadic function f. Accumulation occurs from the left (i.e., starting from the head of the list).

Equations
Instances For
theorem joinM_map_map {m : Type u → Type u} [] [] {α : Type u} {β : Type u} (f : αβ) (a : m (m α)) :
joinM () = f <$> theorem joinM_map_joinM {m : Type u → Type u} [] [] {α : Type u} (a : m (m (m α))) : joinM (joinM <$> a) = joinM ()
@[simp]
theorem joinM_map_pure {m : Type u → Type u} [] [] {α : Type u} (a : m α) :
joinM (pure <$> a) = a @[simp] theorem joinM_pure {m : Type u → Type u} [] [] {α : Type u} (a : m α) : joinM (pure a) = a def succeeds {F : TypeType v} [] {α : Type} (x : F α) : Returns pure true if the computation succeeds and pure false otherwise. Instances For def tryM {F : TypeType v} [] {α : Type} (x : F α) : Attempts to perform the computation, but fails silently if it doesn't succeed. Instances For def try? {F : TypeType v} [] {α : Type} (x : F α) : F () Attempts to perform the computation, and returns none if it doesn't succeed. Instances For @[simp] theorem guard_true {F : TypeType v} [] {h : } : @[simp] theorem guard_false {F : TypeType v} [] {h : } : = failure def Sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} : e α(αe β) → e β The monadic bind operation for Sum. Instances For instance Sum.instMonadSum {e : Type v} : class CommApplicative (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 => y) = Seq.seq () fun x => y • seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun x => y) = Seq.seq ( <$> x) fun x => y
• pure_seq : ∀ {α β : Type u} (g : αβ) (x : m α), (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 : m (αβ)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g • seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (αβ)) (h : m (βγ)), (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
• commutative_prod : ∀ {α β : Type u} (a : m α) (b : m β), (Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => (a, b)) <$> b) fun x => a

Computations performed first on a : α and then on b : β are equal to those performed in the reverse order.

A CommApplicative functor m is a (lawful) applicative functor which behaves identically on α × β and β × α, so computations can occur in either order.

Instances
theorem CommApplicative.commutative_map {m : Type u → Type v} [h : ] [] {α : Type u} {β : Type u} {γ : Type u} (a : m α) (b : m β) {f : αβγ} :
(Seq.seq (f <$> a) fun x => b) = Seq.seq (flip f <$> b) fun x => a