# mathlibdocumentation

control.applicative

theorem applicative.map_seq_map {F : Type uType v} [applicative F] {α β γ σ : Type u} (f : α → β → γ) (g : σ → β) (x : F α) (y : F σ) :
f <$> x <*> g <$> y = f) <$> x <*> y theorem applicative.pure_seq_eq_map' {F : Type uType v} [applicative F] {α β : Type u} (f : α → β) : theorem applicative.ext {F : Type uType u_1} {A1 A2 : applicative F} : (∀ {α : Type u} (x : α), pure x = pure x)(∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x)A1 = A2 @[instance] theorem functor.comp.map_pure {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α β : Type v} (f : α → β) (x : α) : f <$> pure x = pure (f x)

theorem functor.comp.seq_pure {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α β : Type v} (f : G (α → β)) (x : α) :
f <*> pure x = (λ (g : α → β), g x) <$> f theorem functor.comp.seq_assoc {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α β γ : Type v} (x : G α) (f : G (α → β)) (g : G (β → γ)) : g <*> (f <*> x) = <*> x theorem functor.comp.pure_seq_eq_map {F : Type uType w} {G : Type vType u} [applicative F] [applicative G] {α β : Type v} (f : α → β) (x : G α) : pure f <*> x = f <$> x

@[instance]
def functor.comp.is_lawful_applicative {F : Type uType w} {G : Type vType u} [applicative F] [applicative G]  :

theorem functor.comp.applicative_id_comp {F : Type u_1Type u_2} [AF : applicative F] [LF : is_lawful_applicative F] :

theorem functor.comp.applicative_comp_id {F : Type u_1Type u_2} [AF : applicative F] [LF : is_lawful_applicative F] :

@[instance]
def functor.comp.is_comm_applicative {f : Type uType w} {g : Type vType u} [applicative f] [applicative g]  :

theorem comp.seq_mk {α β : Type w} {f : Type uType v} {g : Type wType u} [applicative f] [applicative g] (h : f (g (α → β))) (x : f (g α)) :

@[instance]
def functor.const.applicative {α : Type u_1} [has_one α] [has_mul α] :

Equations
@[instance]
def functor.const.is_lawful_applicative {α : Type u_1} [monoid α] :

@[instance]