mathlib3 documentation

control.basic

theorem functor.map_map {α β γ : Type u} {f : Type u Type v} [functor f] [is_lawful_functor f] (m : α β) (g : β γ) (x : f α) :
g <$> m <$> x = (g m) <$> x
@[simp]
theorem id_map' {α : Type u} {f : Type u Type v} [functor f] [is_lawful_functor f] (x : f α) :
(λ (a : α), a) <$> x = x
def mzip_with {F : Type u Type v} [applicative F] {α₁ α₂ φ : Type u} (f : α₁ α₂ F φ) (ma₁ : list α₁) (ma₂ : list α₂) :
F (list φ)
Equations
def mzip_with' {α β γ : Type u} {F : Type u Type v} [applicative F] (f : α β F γ) :
Equations
@[simp]
theorem pure_id'_seq {α : Type u} {F : Type u Type v} [applicative F] [is_lawful_applicative F] (x : F α) :
has_pure.pure (λ (x : α), x) <*> x = x
theorem seq_map_assoc {α β γ : Type u} {F : Type u Type v} [applicative F] [is_lawful_applicative F] (x : F β)) (f : γ α) (y : F γ) :
x <*> f <$> y = (λ (m : α β), m f) <$> x <*> y
theorem map_seq {α β γ : Type u} {F : Type u Type v} [applicative F] [is_lawful_applicative F] (f : β γ) (x : F β)) (y : F α) :
f <$> (x <*> y) = function.comp f <$> x <*> y
theorem map_bind {α β γ : Type u} {m : Type u Type v} [monad m] [is_lawful_monad m] (x : m α) {g : α m β} {f : β γ} :
f <$> (x >>= g) = x >>= λ (a : α), f <$> g a
theorem seq_bind_eq {α β γ : Type u} {m : Type u Type v} [monad m] [is_lawful_monad m] (x : m α) {g : β m γ} {f : α β} :
f <$> x >>= g = x >>= g f
theorem seq_eq_bind_map {α β : Type u} {m : Type u Type v} [monad m] [is_lawful_monad m] {x : m α} {f : m β)} :
f <*> x = f >>= λ (_x : α β), _x <$> x
@[reducible]
def fish {m : Type u_1 Type u_2} [monad m] {α : Sort u_3} {β γ : Type u_1} (f : α m β) (g : β m γ) (x : α) :
m γ

This is the Kleisli composition

Equations
theorem fish_pure {m : Type u Type v} [monad m] [is_lawful_monad m] {α : Sort u_1} {β : Type u} (f : α m β) :
theorem fish_pipe {m : Type u Type v} [monad m] [is_lawful_monad m] {α β : Type u} (f : α m β) :
theorem fish_assoc {m : Type u Type v} [monad m] [is_lawful_monad m] {α : Sort u_1} {β γ φ : Type u} (f : α m β) (g : β m γ) (h : γ m φ) :
f >=> g >=> h = f >=> (g >=> h)
def list.mmap_accumr {α : Type u} {β' γ' : Type v} {m' : Type v Type w} [monad m'] (f : α β' m' (β' × γ')) :
β' list α m' (β' × list γ')
Equations
def list.mmap_accuml {α : Type u} {β' γ' : Type v} {m' : Type v Type w} [monad m'] (f : β' α m' (β' × γ')) :
β' list α m' (β' × list γ')
Equations
theorem mjoin_map_map {m : Type u Type u} [monad m] [is_lawful_monad m] {α β : Type u} (f : α β) (a : m (m α)) :
theorem mjoin_map_mjoin {m : Type u Type u} [monad m] [is_lawful_monad m] {α : Type u} (a : m (m (m α))) :
@[simp]
theorem mjoin_map_pure {m : Type u Type u} [monad m] [is_lawful_monad m] {α : Type u} (a : m α) :
@[simp]
theorem mjoin_pure {m : Type u Type u} [monad m] [is_lawful_monad m] {α : Type u} (a : m α) :
def succeeds {F : Type Type v} [alternative F] {α : Type} (x : F α) :
Equations
def mtry {F : Type Type v} [alternative F] {α : Type} (x : F α) :
Equations
@[simp]
@[protected]
def sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} :
e α e β) e β
Equations
@[protected, instance]
def sum.monad {e : Type v} :
Equations
@[protected, instance]
@[protected, instance]
@[class]
structure is_comm_applicative (m : Type u_1 Type u_2) [applicative m] :
Prop
Instances of this typeclass
theorem is_comm_applicative.commutative_map {m : Type u_1 Type u_2} [applicative m] [is_comm_applicative m] {α β γ : Type u_1} (a : m α) (b : m β) {f : α β γ} :
f <$> a <*> b = flip f <$> b <*> a