control.applicative - mathlib docs

source

theorem applicative.map_seq_map {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {α β γ σ : Type u} (f : α → β → γ) (g : σ → β) (x : F α) (y : F σ) :

f <$> x <*> g <$> y = (flip function.comp g ∘ f) <$> x <*> y

source

theorem applicative.pure_seq_eq_map' {F : Type u → Type v} [applicative F] [is_lawful_applicative F] {α β : Type u} (f : α → β) :

has_seq.seq (pure f) = functor.map f

source

theorem applicative.ext {F : Type u → Type u_1} {A1 A2 : applicative F} [is_lawful_applicative F] [is_lawful_applicative F] (H1 : ∀ {α : Type u} (x : α), pure x = pure x) (H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x) :

A1 = A2

source

@[protected, instance]

def id.is_comm_applicative :

is_comm_applicative id

source

theorem functor.comp.map_pure {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β : Type v} (f : α → β) (x : α) :

f <$> pure x = pure (f x)

source

theorem functor.comp.seq_pure {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β : Type v} (f : functor.comp F G (α → β)) (x : α) :

f <*> pure x = (λ (g : α → β), g x) <$> f

source

theorem functor.comp.seq_assoc {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β γ : Type v} (x : functor.comp F G α) (f : functor.comp F G (α → β)) (g : functor.comp F G (β → γ)) :

g <*> (f <*> x) = function.comp <$> g <*> f <*> x

source

theorem functor.comp.pure_seq_eq_map {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β : Type v} (f : α → β) (x : functor.comp F G α) :

pure f <*> x = f <$> x

source

@[protected, instance]