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.instAlternative : Alternative List

Equations

• List.instAlternative = { toApplicative := Monad.toApplicative, failure := @List.nil, orElse := fun {α : Type ?u.7} (l : List α) (l' : Unit → List α) => l.append (l' ()) }