Documentation

Mathlib.Init.Data.List.Instances

Decidable Instances for List not (yet) in Std

theorem List.bind_singleton {α : Type u} {β : Type v} (f : αList β) (x : α) :
List.bind [x] f = f x
@[simp]
theorem List.bind_singleton' {α : Type u} (l : List α) :
(List.bind l fun (x : α) => [x]) = l
theorem List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
List.map f l = List.bind l fun (x : α) => [f x]
theorem List.bind_assoc {γ : Type w} {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) (g : βList γ) :
List.bind (List.bind l f) g = List.bind l fun (x : α) => List.bind (f x) g
Equations
Equations
instance List.decidableBex {α : Type u} {p : αProp} [DecidablePred p] (l : List α) :
Decidable (∃ (x : α), x l p x)
Equations
instance List.decidableBall {α : Type u} {p : αProp} [DecidablePred p] (l : List α) :
Decidable (∀ (x : α), x lp x)
Equations