Commits

Anonymous committed a42ca17 Draft

Remove old file (Identity.v)

  • Participants
  • Parent commits 6c64268

Comments (0)

Files changed (1)

src/Identity.v

-Require Import Monads.
-
-(** * Identity monad *)
-Module Identity <: MONAD <: MONADT_RAW.
-
-  Module Raw <: MONADT_RAW.
-
-    Definition m (A : Type) := A.
-    Definition tm := m. (* for MTinfix *)
-
-    Definition ret {A} (x : A) := x.
-
-    Definition bind {A B} (f : A -> m B) (ma : m A) : m B :=
-      f ma.
-
-    Theorem bind_unit : forall A B (a : A) (f : A -> m B),
-      bind f (ret a) = f a
-    .
-    auto.
-    Qed.
-
-    Theorem unit_bind : forall A (ma : m A),
-      bind (@ret A) ma = ma
-    .
-    auto.
-    Qed.
-
-    Theorem bind_bind : forall A B C
-        (ma : m A) (f : A -> m B) (g : B -> m C),
-      bind g (bind f ma)
-      =
-      bind (fun x => bind g (f x)) ma
-    .
-    auto.
-    Qed.
-
-  End Raw.
-
-  Include Raw.
-
-  Module Ops := MTinfix(Raw).
-
-End Identity.