# Documentation

Mathlib.Control.Applicative

# applicative instances #

This file provides Applicative instances for concrete functors:

• id
• Functor.comp
• Functor.const
• Functor.add_const
theorem Applicative.map_seq_map {F : Type u → Type v} [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} {σ : Type u} (f : αβγ) (g : σβ) (x : F α) (y : F σ) :
(Seq.seq (f <$> x) fun x => g <$> y) = Seq.seq ((flip (fun x x_1 => x x_1) g f) <$> x) fun x => y theorem Applicative.pure_seq_eq_map' {F : Type u → Type v} [inst : ] [inst : ] {α : Type u} {β : Type u} (f : αβ) : (fun x x_1 => Seq.seq x fun x => x_1) (pure f) = (fun x x_1 => x <$> x_1) f
theorem Applicative.ext {F : Type u → Type u_1} {A1 : } {A2 : } [inst : ] [inst : ] :
(∀ {α : Type u} (x : α), pure x = pure x) → (∀ {α β : Type u} (f : F (αβ)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x) → A1 = A2
theorem Functor.Comp.map_pure {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : 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} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type v} {β : Type v} (f : Functor.Comp F G (αβ)) (x : α) : (Seq.seq f fun x => pure x) = (fun g => g x) <$> f
theorem Functor.Comp.seq_assoc {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type v} {β : Type v} {γ : Type v} (x : Functor.Comp F G α) (f : Functor.Comp F G (αβ)) (g : Functor.Comp F G (βγ)) :
(Seq.seq g fun x => Seq.seq f fun x => x) = Seq.seq (Seq.seq (Function.comp <$> g) fun x => f) fun x => x theorem Functor.Comp.pure_seq_eq_map {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type v} {β : Type v} (f : αβ) (x : Functor.Comp F G α) : (Seq.seq (pure f) fun x => x) = f <$> x
instance Functor.Comp.instLawfulApplicativeCompInstApplicativeComp {F : Type u → Type w} {G : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
theorem Functor.Comp.applicative_id_comp {F : Type u_1 → Type u_2} [AF : ] [inst : ] :
Functor.Comp.instApplicativeComp = AF
theorem Functor.Comp.applicative_comp_id {F : Type u_1 → Type u_2} [AF : ] [inst : ] :
Functor.Comp.instApplicativeComp = AF
instance Functor.Comp.instCommApplicativeCompInstApplicativeComp {f : Type u → Type w} {g : Type v → Type u} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
theorem Comp.seq_mk {α : Type w} {β : Type w} {f : Type u → Type v} {g : Type w → Type u} [inst : ] [inst : ] (h : f (g (αβ))) (x : f (g α)) :
(Seq.seq () fun x => ) = Functor.Comp.mk (Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <\$> h) fun x => x)
instance instApplicativeConst {α : Type u_1} [inst : One α] [inst : Mul α] :
Equations
• instApplicativeConst = Applicative.mk
instance instApplicativeAddConst {α : Type u_1} [inst : Zero α] [inst : Add α] :
Equations