Documentation

Mathlib.Control.Applicative

applicative instances #

This file provides Applicative instances for concrete functors:

source
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 σ) :
(Seq.seq (f <$> x) fun (x : Unit) => g <$> y) = Seq.seq (((fun (x : β → γ) => x ∘ g) ∘ f) <$> x) fun (x : Unit) => y
source
theorem Applicative.pure_seq_eq_map' {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α : Type u} {β : Type u} (f : α → β) :
(fun (x : F α) => Seq.seq (pure f) fun (x_1 : Unit) => x) = fun (x : F α) => f <$> x
source
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 α), (Seq.seq f fun (x_1 : Unit) => x) = Seq.seq f fun (x_1 : Unit) => x) → A1 = A2
source
instance instCommApplicativeIdToApplicativeInstMonadId :
CommApplicative Id
Equations
source
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)
source
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 : α) :
(Seq.seq f fun (x_1 : Unit) => pure x) = (fun (g : α → β) => g x) <$> f
source
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 (β → γ)) :
(Seq.seq g fun (x_1 : Unit) => Seq.seq f fun (x_2 : Unit) => x) = Seq.seq (Seq.seq (Function.comp <$> g) fun (x : Unit) => f) fun (x_1 : Unit) => x
source
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 α) :
(Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
source
instance Functor.Comp.instLawfulApplicativeComp {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] :
LawfulApplicative (Functor.Comp F G)
Equations
source
theorem Functor.Comp.applicative_id_comp {F : Type u_1 → Type u_2} [AF : Applicative F] [LawfulApplicative F] :
Functor.Comp.instApplicativeComp = AF
source
theorem Functor.Comp.applicative_comp_id {F : Type u_1 → Type u_2} [AF : Applicative F] [LawfulApplicative F] :
Functor.Comp.instApplicativeComp = AF
source
instance Functor.Comp.instCommApplicativeCompInstApplicativeComp {f : Type u → Type w} {g : Type v → Type u} [Applicative f] [Applicative g] [CommApplicative f] [CommApplicative g] :
CommApplicative (Functor.Comp f g)
Equations
source
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 α)) :
(Seq.seq (Functor.Comp.mk h) fun (x_1 : Unit) => Functor.Comp.mk x) = Functor.Comp.mk (Seq.seq ((fun (x : g (α → β)) (x_1 : g α) => Seq.seq x fun (x : Unit) => x_1) <$> h) fun (x_1 : Unit) => x)
source
instance instApplicativeConst {α : Type u_1} [One α] [Mul α] :
Applicative (Functor.Const α)
Equations
  • instApplicativeConst = Applicative.mk
source
instance instLawfulApplicativeConstInstApplicativeConstToOneToMulToMulOneClass {α : Type u_1} [Monoid α] :
LawfulApplicative (Functor.Const α)
Equations
source
instance instApplicativeAddConst {α : Type u_1} [Zero α] [Add α] :
Applicative (Functor.AddConst α)
Equations
  • instApplicativeAddConst = Applicative.mk
source
instance instLawfulApplicativeAddConstInstApplicativeAddConstToZeroToAddToAddSemigroup {α : Type u_1} [AddMonoid α] :
LawfulApplicative (Functor.AddConst α)
Equations