Merge pull request #1360 from RaoulHC/rebindable-do-syntax-docs

Update docs to reflect usage of >> in do syntax

docs/source/tutorial/interfaces.rst

@@ -277,12 +277,18 @@ defined as follows:
     interface Applicative m => Monad (m : Type -> Type) where
         (>>=)  : m a -> (a -> m b) -> m b
 
+There is also a non-binding sequencing operator, defined for ``Monad`` as:
+
+.. code-block:: idris
+
+    v >> e = v >>= \_ => e
+
 Inside a ``do`` block, the following syntactic transformations are
 applied:
 
 - ``x <- v; e`` becomes ``v >>= (\x => e)``
 
-- ``v; e`` becomes ``v >>= (\_ => e)``
+- ``v; e`` becomes ``v >> e``
 
 - ``let x = v; e`` becomes ``let x = v in e``
 
@@ -305,10 +311,10 @@ Using this we can, for example, define a function which adds two
                    y' <- y -- Extract value from y
                    pure (x' + y') -- Add them
 
-This function will extract the values from ``x`` and ``y``, if they
-are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
-``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
-``do`` notation.
+This function will extract the values from ``x`` and ``y``, if they are both
+available, or return ``Nothing`` if one or both are not ("fail fast"). Managing
+the ``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the ``do``
+notation.
 
 ::
 
@@ -318,10 +324,10 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
     Nothing
 
 The translation of ``do`` notation is entirely syntactic, so there is no
-need for the ``(>>=)`` operator to be the operator defined in the ``Monad``
-interface. Idris will, in general, try to disambiguate which ``(>>=)`` you
-mean by type, but you can explicitly choose with qualified do notation,
-for example:
+need for the ``(>>=)`` and ``(>>)`` operators to be the operator defined in the
+``Monad`` interface. Idris will, in general, try to disambiguate which
+operators you mean by type, but you can explicitly choose with qualified do
+notation, for example:
 
 .. code-block:: idris
 
@@ -331,8 +337,8 @@ for example:
                    y' <- y -- Extract value from y
                    pure (x' + y') -- Add them
 
-The ``Prelude.do`` means that Idris will use the ``(>>=)`` operator defined
-in the ``Prelude``.
+The ``Prelude.do`` means that Idris will use the ``(>>=)`` and ``(>>)``
+operators defined in the ``Prelude``.
 
 Pattern Matching Bind
 ~~~~~~~~~~~~~~~~~~~~~