mathlib3 documentation

control.applicative

applicative instances #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides applicative instances for concrete functors:

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 (has_pure.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 : α), has_pure.pure x = has_pure.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 <$> has_pure.pure x = has_pure.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 <*> has_pure.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 α) :
has_pure.pure f <*> x = f <$> x
source
@[protected, instance]
def functor.comp.is_lawful_applicative {F : Type u → Type w} {G : Type v → Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] :
is_lawful_applicative (functor.comp F G)
source
theorem functor.comp.applicative_id_comp {F : Type u_1 → Type u_2} [AF : applicative F] [LF : is_lawful_applicative F] :
functor.comp.applicative = AF
source
theorem functor.comp.applicative_comp_id {F : Type u_1 → Type u_2} [AF : applicative F] [LF : is_lawful_applicative F] :
functor.comp.applicative = AF
source
@[protected, instance]
def functor.comp.is_comm_applicative {f : Type u → Type w} {g : Type v → Type u} [applicative f] [applicative g] [is_comm_applicative f] [is_comm_applicative g] :
is_comm_applicative (functor.comp f g)
source
theorem comp.seq_mk {α β : 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 (has_seq.seq <$> h <*> x)
source
@[protected, instance]
def functor.const.applicative {α : Type u_1} [has_one α] [has_mul α] :
applicative (functor.const α)
Equations
source
@[protected, instance]
def functor.const.is_lawful_applicative {α : Type u_1} [monoid α] :
is_lawful_applicative (functor.const α)
source
@[protected, instance]
def functor.add_const.applicative {α : Type u_1} [has_zero α] [has_add α] :
applicative (functor.add_const α)
Equations
source
@[protected, instance]
def functor.add_const.is_lawful_applicative {α : Type u_1} [add_monoid α] :
is_lawful_applicative (functor.add_const α)