Commits

Anonymous committed 2edde6e

Fix compilation problem

Comments (0)

Files changed (3)

 
 Module Error (Et : ERR_TYPE)
 <: MONAD
-<: ERROR_T (Et) (Identity).
+<: ERROR_T (Et) (Identity.Identity).
 
-  Module Impl := ErrorT (Et) (Identity).
+  Module Impl := ErrorT (Et) (Identity.Identity).
 
   Include Impl.
 
 Require Import Monads.
 
 (** * Identity monad *)
-Module Identity <: MONAD.
+Module Identity <: MONAD <: MONADT_RAW.
 
   Module Raw <: MONADT_RAW.
 
     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 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 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.
+    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.
 
 
   Module Ops := MTinfix(Raw).
 
-(*
-    Notation "m >>= f" := (@bind _ _ f m)
-      (at level 57, right associativity)
-    .
-*)
-
 End Identity.
 End StateT.
 
 
-(* TODO: This does not compile for some reason *)
+(** * Standard instance of State Monad *)
+Module State (St : ST_TYPE) <: MONAD.
 
-(** * Standard instance of State Monad *)
-(* Module State (St : ST_TYPE) <: MONAD. *)
+  Module Impl := StateT (St) (Identity.Identity).
 
-(*   Module Impl := StateT (St) (Identity). *)
+  Include Impl.
 
-(*   Include Impl. *)
+End State.
 
-(* End State. *)
 
 
+(** * Example *)
+Module MyState <: ST_TYPE.
+  Definition S := nat.
+End MyState.
 
-(* (** * Example *) *)
-(* Module MyState <: ST_TYPE. *)
-(*   Definition S := nat. *)
-(* End MyState. *)
+Module State_nat := StateT (MyState) (Identity.Identity).
+Import State_nat.
+Import Ops.
 
-(* Module State_nat := StateT (MyState) (Identity). *)
-(* Import State_nat. *)
-(* Import Ops. *)
-
-(* Eval compute in *)
-(*   ( run_state *)
-(*       5 *)
-(*       ( a <- ret 3;; *)
-(*         b <- get;; *)
-(*         put $ a + b;; *)
-(*         c <- get;; *)
-(*         ret $ c + 4 *)
-(*       ) *)
-(*   ). *)
-(* *)
+Eval compute in
+  ( run_state
+      5
+      ( a <- ret 3;;
+        b <- get;;
+        put $ a + b;;
+        c <- get;;
+        ret $ c + 4
+      )
+  ).