# mathlibdocumentation

control.basic

Simp set for functor_norm

theorem functor.map_map {α β γ : Type u} {f : Type uType v} [functor f] (m : α → β) (g : β → γ) (x : f α) :
g <$> m <$> x = (g m) <$> x @[simp] theorem id_map' {α : Type u} {f : Type uType v} [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 β
Equations
@[simp]
theorem pure_id'_seq {α : Type u} {F : Type uType v} [applicative F] (x : F α) :
has_pure.pure (λ (x : α), x) <*> x = x
theorem seq_map_assoc {α β γ : Type u} {F : Type uType v} [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] (f : β → γ) (x : F (α → β)) (y : F α) :
f <$> (x <*> y) = <*> 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] (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] (x : m α) {g : β → m γ} {f : α → β} : f <$> x >>= g = x >>= g f
theorem seq_eq_bind_map {α β : Type u} {m : Type uType v} [monad m] {x : m α} {f : m (α → β)} :
f <*> x = f >>= λ (_x : α → β), _x <$> x @[reducible] 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] {α : Sort u_1} {β : Type u} (f : α → m β) : theorem fish_pipe {m : Type uType v} [monad m] {α β : Type u} (f : α → m β) : theorem fish_assoc {m : Type uType v} [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 • (x :: xs) = xs >>= λ (_p : β' × list γ'), list.mmap_accumr._match_2 f x _p • = has_pure.pure (a, list.nil γ') • list.mmap_accumr._match_2 f x (a', ys) = f x a' >>= λ (_p : β' × γ'), list.mmap_accumr._match_1 ys _p • list.mmap_accumr._match_1 ys (a'', y) = has_pure.pure (a'', y :: ys) def list.mmap_accuml {α : Type u} {β' γ' : Type v} {m' : Type vType w} [monad m'] (f : β' → α → m' (β' × γ')) : β' → list αm' (β' × list γ') Equations • (x :: xs) = f a x >>= λ (_p : β' × γ'), list.mmap_accuml._match_2 (λ (a' : β'), a' xs) _p • = has_pure.pure (a, list.nil γ') • list.mmap_accuml._match_2 _f_1 (a', y) = _f_1 a' >>= λ (_p : β' × list γ'), list.mmap_accuml._match_1 y _p • list.mmap_accuml._match_1 y (a'', ys) = has_pure.pure (a'', y :: ys) theorem mjoin_map_map {m : Type uType u} [monad m] {α β : Type u} (f : α → β) (a : m (m α)) : mjoin <$> a) = f <$> theorem mjoin_map_mjoin {m : Type uType u} [monad m] {α : Type u} (a : m (m (m α))) : @[simp] theorem mjoin_map_pure {m : Type uType u} [monad m] {α : Type u} (a : m α) : = a @[simp] theorem mjoin_pure {m : Type uType u} [monad m] {α : Type u} (a : m α) : = 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 • to_is_lawful_applicative : • commutative_prod : ∀ {α β : Type ?} (a : m α) (b : m β), <*> b = (λ (b : β) (a : α), (a, b)) <$> b <*> a
Instances of this typeclass
theorem is_comm_applicative.commutative_map {m : Type u_1Type u_2} [applicative m] {α β γ : Type u_1} (a : m α) (b : m β) {f : α → β → γ} :
f <$> a <*> b = flip f <$> b <*> a