Decidable and Monad instances for List not (yet) in Batteries

theorem List.bind_singleton {α : Type u} {β : Type v} (f : α → List β) (x : α) : [x].bind f = f x

@[simp]

theorem List.bind_singleton' {α : Type u} (l : List α) : (l.bind fun (x : α) => [x]) = l

theorem List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l = l.bind fun (x : α) => [f x]

theorem List.bind_assoc {γ : Type w} {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) (g : β → List γ) : (l.bind f).bind g = l.bind fun (x : α) => (f x).bind g

instance List.instMonad : Monad List

Equations

• List.instMonad = Monad.mk

@[simp]

theorem List.pure_def {α : Type u} (a : α) : pure a = [a]

instance List.instLawfulMonad : LawfulMonad List

Equations

• List.instLawfulMonad = ⋯

instance List.instAlternative : Alternative List

Equations

• List.instAlternative = Alternative.mk @List.nil fun {α : Type u} (l : List α) (l' : Unit → List α) => l.append (l' ())