Move Data.Monads.ListMonad to Data.List

coq-community · Jan 19, 2022 · affdcd1 · affdcd1
1 parent ea8a862
commit affdcd1
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 20 deletions.
diff --git 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
@@ -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