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

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' ())