Notation ;; should be right associative

Author: liyishuai

.circleci/config.yml

@@ -2,10 +2,13 @@ version: 2.1
 
 defaults: &defaults
   environment:
+    OPAMBESTEFFORT: true
+    OPAMJOBS: 2
     OPAMVERBOSE: 1
     OPAMWITHTEST: true
     OPAMYES: true
     TERM: xterm
+  resource_class: medium
 
 commands:
   startup:
@@ -44,17 +47,17 @@ commands:
         command: opam uninstall .
     - run:
         name: Build and test locally
-        command: make
+        command: make -j`nproc`
     - run:
         name: Cleanup local directory
         command: |
-          make clean
+          make -j`nproc` clean
           ls -AGR
   deploy:
     steps:
     - run:
         name: Build Documentation
-        command: make html
+        command: make -j`nproc` html
     - run:
         name: Configure Git
         command: |

scratch/notation.md

@@ -4,10 +4,10 @@ Module | Notation | Definition | Level | Associativity
 `FunctorNotation` | `f <$> x` | `fmap f x` | 52 | left
 `ApplicativeNotation` | `f <*> x` | `ap f x` | 52 | left
 `MonadPlusNotation` | `x <+> y` | `mplus x y` | 54 | left
+`MonadNotation` | `c >>= f` | `bind c f` | 58 | left
 `MonadNotation` | `f =<< c` | `bind c f` | 61 | right
 `MonadNotation` | `f >=> g` | `mcompose f g` | 61 | right
 `MonadNotation` | `x <- c1 ;; c2` | `bind c1 (fun x => c2)` | 61 | right
 `MonadNotation` | `' pat <- c1 ;; c2` | `bind c1 (fun x => match x with pat => c2)` | 61 | right
-`MonadNotation` | `c >>= f` | `bind c f` | 62 | left
-`MonadNotation` | `e1 ;; e2` | `_ <- e1 ;; e2` | 62 | left
+`MonadNotation` | `e1 ;; e2` | `_ <- e1 ;; e2` | 61 | right
 `FunNotation` | `f $ x` | `f x` | 99 | right

theories/Structures/Monad.v

@@ -53,15 +53,15 @@ Module MonadNotation.
 
   Delimit Scope monad_scope with monad.
 
-  Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 62, left associativity) : monad_scope.
+  Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 58, left associativity) : monad_scope.
   Notation "f =<< c" := (@bind _ _ _ _ c f) (at level 61, right associativity) : monad_scope.
   Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope.
 
   Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2))
     (at level 61, c1 at next level, right associativity) : monad_scope.
 
   Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad
-    (at level 62, left associativity) : monad_scope.
+    (at level 61, right associativity) : monad_scope.
 
   Notation "' pat <- c1 ;; c2" :=
     (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))