# 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_1 : Unit) => 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 : Unit) => f <$> y) = Seq.seq ((fun (x : αβ) => x f) <$> x) fun (x : Unit) => 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 : Unit) => y) = Seq.seq ((fun (x : αβ) => f x) <$> x) fun (x : Unit) => 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 ax 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 ( <$> a) = f <$>
theorem joinM_map_joinM {m : Type u → Type u} [] [] {α : Type u} (a : m (m (m α))) :
joinM (joinM <$> a) = joinM (joinM a) @[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.

Equations
Instances For
def tryM {F : TypeType v} [] {α : Type} (x : F α) :

Attempts to perform the computation, but fails silently if it doesn't succeed.

Equations
Instances For
def try? {F : TypeType v} [] {α : Type} (x : F α) :
F (Option α)

Attempts to perform the computation, and returns none if it doesn't succeed.

Equations
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.

Equations
• x✝.bind x = match x✝, x with | , x_1 => | , f => f x
Instances For
instance Sum.instMonad_mathlib {e : Type v} :
Equations
Equations
• =
Equations
• =
class CommApplicative (m : Type u → Type v) [] extends :

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

• 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 ( <$> x) 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
• commutative_prod : ∀ {α β : Type u} (a : m α) (b : m β), (Seq.seq (Prod.mk <$> a) fun (x : Unit) => b) = Seq.seq ((fun (b : β) (a : α) => (a, b)) <$> b) fun (x : Unit) => a

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

Instances
theorem CommApplicative.commutative_prod {m : Type u → Type v} [] [self : ] {α : Type u} {β : Type u} (a : m α) (b : m β) :
(Seq.seq (Prod.mk <$> a) fun (x : Unit) => b) = Seq.seq ((fun (b : β) (a : α) => (a, b)) <$> b) fun (x : Unit) => a

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

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 : Unit) => b) = Seq.seq (flip f <$> b) fun (x : Unit) => a