Documentation

Mathlib.Control.Applicative

applicative instances #

This file provides Applicative instances for concrete functors:

theorem Applicative.map_seq_map {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α : Type u} {β : Type u} {γ : Type u} {σ : Type u} (f : αβγ) (g : σβ) (x : F α) (y : F σ) :
f <$> x <*> g <$> y = ((fun (x : βγ) => x g) f) <$> x <*> y
theorem Applicative.pure_seq_eq_map' {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α : Type u} {β : Type u} (f : αβ) :
(fun (x : F α) => pure f <*> x) = fun (x : F α) => f <$> x
theorem Applicative.ext {F : Type u → Type u_1} {A1 : Applicative F} {A2 : Applicative F} [LawfulApplicative F] [LawfulApplicative F] :
(∀ {α : Type u} (x : α), pure x = pure x)(∀ {α β : Type u} (f : F (αβ)) (x : F α), f <*> x = f <*> x)A1 = A2
theorem Functor.Comp.map_pure {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α : Type v} {β : Type v} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
theorem Functor.Comp.seq_pure {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α : Type v} {β : Type v} (f : Functor.Comp F G (αβ)) (x : α) :
f <*> pure x = (fun (g : αβ) => g x) <$> f
theorem Functor.Comp.seq_assoc {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α : Type v} {β : Type v} {γ : 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
theorem Functor.Comp.pure_seq_eq_map {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α : Type v} {β : Type v} (f : αβ) (x : Functor.Comp F G α) :
pure f <*> x = f <$> x
theorem Functor.Comp.applicative_id_comp {F : Type u_1 → Type u_2} [AF : Applicative F] [LawfulApplicative F] :
Functor.Comp.instApplicativeComp = AF
theorem Functor.Comp.applicative_comp_id {F : Type u_1 → Type u_2} [AF : Applicative F] [LawfulApplicative F] :
Functor.Comp.instApplicativeComp = AF
theorem Comp.seq_mk {α : Type w} {β : Type w} {f : Type u → Type v} {g : Type w → Type u} [Applicative f] [Applicative g] (h : f (g (αβ))) (x : f (g α)) :
Functor.Comp.mk h <*> Functor.Comp.mk x = Functor.Comp.mk ((fun (x1 : g (αβ)) (x2 : g α) => x1 <*> x2) <$> h <*> x)
Equations
  • instApplicativeConstOfOneOfMul = Applicative.mk
Equations
  • =
Equations
  • instApplicativeAddConstOfZeroOfAdd = Applicative.mk