Monad instances for List

instance List.instMonad : Monad List

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

instance List.instLawfulMonad : LawfulMonad List

instance List.instAlternativeMonad_mathlib : AlternativeMonad List

Equations

• One or more equations did not get rendered due to their size.

instance List.instLawfulAlternative_mathlib : LawfulAlternative List