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:

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
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
@[protected, instance]
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 : α) :
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
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
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 α) :
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 α)) :
@[protected, instance]
Equations
@[protected, instance]