Documentation

Mathlib.Data.List.Monad

Monad instances for List #

source
🔸 coverage
@[implicit_reducible]
instance List.instMonad :
Monad List
source
📐 coverage
@[simp]
theorem List.pure_def {α : Type u} (a : α) :
pure a = [a]
source
📐 coverage
instance List.instLawfulMonad :
LawfulMonad List
source
🔸 coverage
@[implicit_reducible]
instance List.instAlternativeMonad_mathlib :
AlternativeMonad List
source
📐 coverage
instance List.instLawfulAlternative_mathlib :
LawfulAlternative List