Commits

wojc...@gmail.com  committed 68d6803

Add needed module type constraint

  • Participants
  • Parent commits 395a06e

Comments (0)

Files changed (2)

File src/Monads.v

 
 
 (** * Monad transformer from monad *)
-Module Type MONADT (M : MONAD) <: MONAD.
+Module Type MONADT (M : MONAD) <: MONAD <: MONADT_RAW.
 
   Module Mo.
   Parameter tm : Type -> Type.

File src/StateMonad.v

 End StateT.
 
 
+(* TODO: This does not compile for some reason *)
+
 (** * Standard instance of State Monad *)
-Module State (St : ST_TYPE) <: MONAD.
+(* Module State (St : ST_TYPE) <: MONAD. *)
 
-  Module Impl := StateT (St) (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).
-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 *)
+(*       ) *)
+(*   ). *)
+(* *)