Monad instances for List

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

instance List.instAlternative : Alternative List

Equations

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