Move Data.Monads.ListMonad to Data.List

Author: liyishuai

_CoqProject

@@ -119,7 +119,6 @@ theories/Data/Monads/FuelMonadLaws.v
 theories/Data/Monads/FuelMonad.v
 theories/Data/Monads/IdentityMonadLaws.v
 theories/Data/Monads/IdentityMonad.v
-theories/Data/Monads/ListMonad.v
 theories/Data/Monads/OptionMonadLaws.v
 theories/Data/Monads/OptionMonad.v
 theories/Data/Monads/ReaderMonadLaws.v

theories/Data/List.v

@@ -98,7 +98,7 @@ Global Instance Foldable_list@{u} {T : Type@{u}} : Foldable (list T) T :=
 
 Require Import ExtLib.Structures.Traversable.
 Require Import ExtLib.Structures.Functor.
-Require Import ExtLib.Structures.Monad.
+Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.Applicative.
 
 Section traversable.
@@ -120,10 +120,16 @@ Global Instance Traversable_list@{} : Traversable list :=
 
 Monomorphic Universe listU.
 
-Global Instance Monad_list@{} : Monad@{listU listU} list :=
-{ ret  := fun _ x => x :: nil
-; bind := fun _ _ x f =>
-  List.fold_right (fun x acc => f x ++ acc) nil x
+Global Instance Monad_list : Monad list :=
+{ ret := fun _ v => v :: nil
+; bind := fun _ _ l f => flat_map f l
+}.
+
+Global Instance MonadZero_list : MonadZero list :=
+{ mzero := @nil }.
+
+Global Instance MonadPlus_list : MonadPlus list :=
+{ mplus _A _B a b := List.map inl a ++ List.map inr b
 }.
 
 Section list.