mathlib documentation

control.basic

Simp set for functor_norm

theorem functor.map_map {α β γ : Type u} {f : Type uType v} [functor f] [is_lawful_functor f] (m : α → β) (g : β → γ) (x : f α) :
g <$> m <$> x = (g m) <$> x

@[simp]
theorem id_map' {α : Type u} {f : Type uType v} [functor f] [is_lawful_functor f] (x : f α) :
(λ (a : α), a) <$> x = x

def mzip_with {F : Type uType v} [applicative F] {α₁ α₂ φ : Type u} :
(α₁ → α₂ → F φ)list α₁list α₂F (list φ)

Equations
def mzip_with' {α β γ : Type u} {F : Type uType v} [applicative F] :
(α → β → F γ)list αlist βF punit

Equations
@[simp]
theorem pure_id'_seq {α : Type u} {F : Type uType v} [applicative F] [is_lawful_applicative F] (x : F α) :
pure (λ (x : α), x) <*> x = x

theorem seq_map_assoc {α β γ : Type u} {F : Type uType v} [applicative F] [is_lawful_applicative F] (x : F (α → β)) (f : γ → α) (y : F γ) :
x <*> f <$> y = (λ (m : α → β), m f) <$> x <*> y

theorem map_seq {α β γ : Type u} {F : Type uType v} [applicative F] [is_lawful_applicative F] (f : β → γ) (x : F (α → β)) (y : F α) :
f <$> (x <*> y) = function.comp f <$> x <*> y

def list.mpartition {f : Type → Type} [monad f] {α : Type} :
(α → f bool)list αf (list α × list α)

Equations
theorem map_bind {α β γ : Type u} {m : Type uType v} [monad m] [is_lawful_monad m] (x : m α) {g : α → m β} {f : β → γ} :
f <$> (x >>= g) = x >>= λ (a : α), f <$> g a

theorem seq_bind_eq {α β γ : Type u} {m : Type uType v} [monad m] [is_lawful_monad m] (x : m α) {g : β → m γ} {f : α → β} :
f <$> x >>= g = x >>= g f

theorem seq_eq_bind_map {α β : Type u} {m : Type uType v} [monad m] [is_lawful_monad m] {x : m α} {f : m (α → β)} :
f <*> x = f >>= λ (_x : α → β), _x <$> x

def fish {m : Type u_1Type u_2} [monad m] {α : Sort u_3} {β γ : Type u_1} :
(α → m β)(β → m γ)α → m γ

This is the Kleisli composition

Equations
theorem fish_pure {m : Type uType v} [monad m] [is_lawful_monad m] {α : Sort u_1} {β : Type u} (f : α → m β) :
f >=> pure = f

theorem fish_pipe {m : Type uType v} [monad m] [is_lawful_monad m] {α β : Type u} (f : α → m β) :
pure >=> f = f

theorem fish_assoc {m : Type uType v} [monad m] [is_lawful_monad m] {α : Sort u_1} {β γ φ : Type u} (f : α → m β) (g : β → m γ) (h : γ → m φ) :
f >=> g >=> h = f >=> (g >=> h)

def list.mmap_accumr {α : Type u} {β' γ' : Type v} {m' : Type vType w} [monad m'] :
(α → β' → m' (β' × γ'))β' → list αm' (β' × list γ')

Equations
def list.mmap_accuml {α : Type u} {β' γ' : Type v} {m' : Type vType w} [monad m'] :
(β' → α → m' (β' × γ'))β' → list αm' (β' × list γ')

Equations
theorem mjoin_map_map {m : Type uType u} [monad m] [is_lawful_monad m] {α β : Type u} (f : α → β) (a : m (m α)) :

theorem mjoin_map_mjoin {m : Type uType u} [monad m] [is_lawful_monad m] {α : Type u} (a : m (m (m α))) :

@[simp]
theorem mjoin_map_pure {m : Type uType u} [monad m] [is_lawful_monad m] {α : Type u} (a : m α) :
mjoin (pure <$> a) = a

@[simp]
theorem mjoin_pure {m : Type uType u} [monad m] [is_lawful_monad m] {α : Type u} (a : m α) :
mjoin (pure a) = a

def succeeds {F : Type → Type v} [alternative F] {α : Type} :
F αF bool

Equations
def mtry {F : Type → Type v} [alternative F] {α : Type} :
F αF unit

Equations
@[simp]
theorem guard_true {F : Type → Type v} [alternative F] {h : decidable true} :

@[simp]
theorem guard_false {F : Type → Type v} [alternative F] {h : decidable false} :

def sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} :
e α(α → e β)e β

Equations
@[instance]
def sum.monad {e : Type v} :

Equations
@[instance]
def sum.is_lawful_functor {e : Type v} :

@[instance]
def sum.is_lawful_monad {e : Type v} :

@[class]
structure is_comm_applicative (m : Type u_1Type u_2) [applicative m] :
Prop

Instances
theorem is_comm_applicative.commutative_map {m : Type u_1Type u_2} [applicative m] [is_comm_applicative m] {α β γ : Type u_1} (a : m α) (b : m β) {f : α → β → γ} :
f <$> a <*> b = flip f <$> b <*> a