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 : α₁ → α₂ → F φ) (ma₁ : list α₁) (ma₂ : list α₂) :
F (list φ)
Equations
def mzip_with' {α β γ : Type u} {F : Type uType v} [applicative F] (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} (p : α → 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} (f : α → m β) (g : β → m γ) (x : α) :
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'] (f : α → β' → m' (β' × γ')) :
β' → list αm' (β' × list γ')
Equations
def list.mmap_accuml {α : Type u} {β' γ' : Type v} {m' : Type vType w} [monad m'] (f : β' → α → 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} (x : F α) :
Equations
def mtry {F : Type → Type v} [alternative F] {α : Type} (x : F α) :
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} :
@[protected]
def sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} :
e α(α → e β)e β
Equations
@[protected, instance]
def sum.monad {e : Type v} :
Equations
@[protected, instance]
def sum.is_lawful_functor {e : Type v} :
@[protected, 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