From affdcd19c7cbae16a11e2d6ebf02df0027efed14 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Wed, 12 Jan 2022 16:19:37 -0500
Subject: [PATCH] Move Data.Monads.ListMonad to Data.List

---
 _CoqProject                      |  1 -
 theories/Data/List.v             | 11 +++++++++--
 theories/Data/Monads/ListMonad.v | 17 -----------------
 3 files changed, 9 insertions(+), 20 deletions(-)
 delete mode 100644 theories/Data/Monads/ListMonad.v

diff --git a/_CoqProject b/_CoqProject
index 5aa5e542..5930a73a 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/Data/List.v b/theories/Data/List.v
index 03e4fabe..4de1f73c 100644
--- a/theories/Data/List.v
+++ b/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.
@@ -123,7 +123,14 @@ 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
+  flat_map f x
+}.
+
+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.
diff --git a/theories/Data/Monads/ListMonad.v b/theories/Data/Monads/ListMonad.v
deleted file mode 100644
index a3cc69c6..00000000
--- a/theories/Data/Monads/ListMonad.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import ExtLib.Structures.Monads.
-Require Import List.
-
-Set Implicit Arguments.
-Set Strict Implicit.
-
-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
-}.