Commits

wojc...@gmail.com  committed a94fea3 Draft

Few more tweaks for documentation

  • Participants
  • Parent commits 2796d67

Comments (0)

Files changed (2)

File src/Monads.v

 
 End Minfix.
 
-(** TODO *)
+(** * Infix notations for monad transformers *)
 Module MTinfix (M : MONADT_RAW).
-  Module F <: For_infix.
+  Module F <: For_infix.d
     Include M.
     Definition m := tm.
   End F.

File src/StateMonad.v

 Require Import IdentityMonad.
+Require Import Monads.
+
 (**
 State Monad is a monad encapsulating state between computations.
 
 Usage:
 
-    Require Import StateMonad.
+    [Require Import StateMonad.
 
     Module MyState <: ST_TYPE.
       Definition S := <type_of_my_state>.
-    End MyState.
+    End MyState.]
 
 1. Transformer:
 
-    Module State_my := StateT (MyState) (InnerMonad).
+    [Module State_my := StateT (MyState) (InnerMonad).
     Import State_my.  (* for functions *)
-    Import Ops.  (* for notations *)
+    Import Ops.  (* for notations *)]
 
 2. Monad:
 
-    Module State_my := State (MyState).
+    [Module State_my := State (MyState).
     Import State_my.  (* for functions *)
-    Import Ops.  (* for notations *)
+    Import Ops.  (* for notations *)]
 
 
 Specific functions:
 
-  - get : m S
-  - put : S -> m unit
-  - run_state : S (*initial state*) -> m A -> InnerMonad.m (A * S)
+  - [get : m S]
+  - [put : S -> m unit]
+  - [run_state : S (*initial state*) -> m A -> InnerMonad.m (A * S)]
 *)
 
-Require Import Monads.
-
-(** * Signature for the module that holds the state *)
+(** * Signature for a state *)
 Module Type ST_TYPE.
+  (** Carier for a state *)
   Parameter S : Type.
 End ST_TYPE.
 
 
-(** * Create a monad transformer from state and monad *)
+(** * Signature for a transformer *)
 Module Type MONADT_S (S : ST_TYPE) (M : MONAD).
   Include MONADT (M).
 End MONADT_S.
   .
   Global Implicit Arguments bind [A B].
 
+  (** ** Standard monadic laws
+   Please see Standard monadic laws in Monads.v
+   TODO: how to hyperlink it? *)
   Require Import FunctionalExtensionality.
 
-  (** ** Standard monadic laws *)
   Theorem bind_unit : forall A B (a : A) (f : A -> tm B),
     bind f (ret a) = f a
   .
   Require Import FunctionalExtensionality.
 
   (** ** Monad transfomer laws  *)
+
+  (** Lifting monadic value yields the same monadic value *)
   Theorem lift_ret : forall A (x : A),
     lift (M.ret x) = (ret x)
   .
 
   Module Bc := BindCompose(M).
 
+  (** TODO *)
   Theorem lift_bind : forall A B
       (ma : M.m A) (f : A -> M.m B),
     lift (M.bind f ma) = bind (fun x => lift (f x)) (lift ma)
   .
 
 
-  (** Getting the value *)
+  (** Getting back the value *)
   Definition get : m Stt.S :=
     fun s =>
       M.ret (s, s)