Commits

wojc...@gmail.com  committed cc78a4b Draft

Replace the [Section] mechanism for implicit arguments with a newer syntax

  • Participants
  • Parent commits a94fea3

Comments (0)

Files changed (1)

File src/Monads.v

 
 (** * Infix notations for monad transformers *)
 Module MTinfix (M : MONADT_RAW).
-  Module F <: For_infix.d
+  Module F <: For_infix.
     Include M.
     Definition m := tm.
   End F.
   Module Ops := MTinfix(M).
   Import Ops.
 
-  (** Evaluate each action in the sequence from left to right, and collect
+    (** Evaluate each action in the sequence from left to right, and collect
       the results. *)
-  Section sequence.
-    Variable A : Type.
-    Definition sequence (l : list (tm A)) : tm (list A) :=
-      let f (m : tm A) (m' : tm (list A)) : tm (list A) :=
-          x <- m;;
+  Definition sequence {A} (l : list (tm A)) : tm (list A) :=
+    let f (m : tm A) (m' : tm (list A)) : tm (list A) :=
+        x <- m;;
           y <- m';;
           ret (x :: y)
-      in
-      List.fold_right f (ret nil) l.
-  End sequence.
+    in
+    List.fold_right f (ret nil) l.
 
   (** Evaluate each action in the sequence from left to right, and ignore
       the results. *)
-  Section sequence_.
-    Variable A : Type.
-    Definition sequence_ (l : list (tm A)) : tm unit :=
-      let f x y :=
-          x ;;
+  Definition sequence_ {A} (l : list (tm A)) : tm unit :=
+    let f x y :=
+        x ;;
           y
-      in
-      List.fold_right f (ret tt) l.
-  End sequence_.
+    in
+    List.fold_right f (ret tt) l.
 
   (** [mapM f l] is equivalent to [sequence (map f l)]. *)
-  Section mapM.
-    Variable A B : Type.
-    Definition mapM (f: A -> tm B) (l: list A) : tm (list B) :=
-      @sequence _ (List.map f l)
-    .
-  End mapM.
+  Definition mapM {A B} (f: A -> tm B) (l: list A) : tm (list B) :=
+    @sequence _ (List.map f l)
+  .
 
   (** [mapM_ f l] is equivalent to [sequence_ (map f l)]. *)
-  Section mapM_.
-    Variable A B : Type.
-    Definition mapM_ (f: A -> tm B) (l: list A) : tm unit :=
-      @sequence_ _ (List.map f l)
-    .
-  End mapM_.
+  Definition mapM_ {A B} (f: A -> tm B) (l: list A) : tm unit :=
+    @sequence_ _ (List.map f l)
+  .
 
   (** [forM] is [mapM] with its arguments flipped. *)
-  Section forM.
-    Variable A B : Type.
-    Definition forM (l: list A) (f: A -> tm B) : tm (list B) :=
-      @mapM _ _ f l.
-  End forM.
+  Definition forM {A B} (l: list A) (f: A -> tm B) : tm (list B) :=
+    @mapM _ _ f l.
 
   (** [forM_] is [mapM_] with its arguments flipped. *)
-  Section forM_.
-    Variable A B : Type.
-    Definition forM_ (l: list A) (f: A -> tm B) : tm unit :=
-      @mapM_ _ _ f l.
-  End forM_.
+  Definition forM_ {A B} (l: list A) (f: A -> tm B) : tm unit :=
+    @mapM_ _ _ f l.
 
 End Basics.