Documentation

Mathlib.Data.List.Monad

Monad instances for List #

source
instance List.instMonad :
Monad List
Equations
    source
    @[simp]
    theorem List.pure_def {α : Type u} (a : α) :
    pure a = [a]
    source
    instance List.instLawfulMonad :
    LawfulMonad List
    source
    instance List.instAlternative :
    Alternative List
    Equations