From 2a4197e909330d8dbab87862559d4f7bf7876f31 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Thu, 3 Jun 2021 18:49:31 +0300
Subject: [PATCH] [ doc ] Some documentation on `:=` syntax of `let` bindings
 (#1487)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
---
 docs/source/tutorial/typesfuns.rst | 45 ++++++++++++++++++++++++++++++
 docs/source/updates/updates.rst    |  3 ++
 2 files changed, 48 insertions(+)

diff --git a/docs/source/tutorial/typesfuns.rst b/docs/source/tutorial/typesfuns.rst
index a315c67df..06bdd1f9b 100644
--- a/docs/source/tutorial/typesfuns.rst
+++ b/docs/source/tutorial/typesfuns.rst
@@ -1182,6 +1182,8 @@ Or even:
 More Expressions
 ================
 
+.. _sect-let-bindings:
+
 ``let`` bindings
 ----------------
 
@@ -1205,6 +1207,49 @@ pattern matching at the top level:
     showPerson p = let MkPerson name age = p in
                        name ++ " is " ++ show age ++ " years old"
 
+These let bindings can be annotated with a type:
+
+.. code-block:: idris
+
+   mirror : List a -> List a
+   mirror xs = let xs' : List a = reverse xs in
+                   xs ++ xs'
+
+We can also use the symbol ``:=`` instead of ``=`` to, among other things,
+avoid ambiguities with propositional equality:
+
+.. code-block:: idris
+
+   Diag : a -> Type
+   Diag v = let ty : Type := v = v in ty
+
+Local definitions can also be introduced using ``let``. Just like top level
+ones and ones defined in a ``where`` clause you need to:
+
+1. declare the function and its type
+2. define the function by pattern matching
+
+.. code-block:: idris
+
+   foldMap : Monoid m => (a -> m) -> Vect n a -> m
+   foldMap f = let fo : m -> a -> m
+                   fo ac el = ac <+> f el
+                in foldl fo neutral
+
+The symbol ``:=`` cannot be used in a local function definition. Which means
+that it can be used to interleave let bindings and local definitions without
+introducing ambiguities.
+
+.. code-block:: idris
+
+   foldMap : Monoid m => (a -> m) -> Vect n a -> m
+   foldMap f = let fo : m -> a -> m
+                   fo ac el = ac <+> f el
+                   initial := neutral
+                    --     ^ this indicates that `initial` is a separate binding,
+                    -- not relevant to definition of `fo`
+                in foldl fo initial
+
 List comprehensions
 -------------------
 
diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst
index bb6174b84..3a95a8e18 100644
--- a/docs/source/updates/updates.rst
+++ b/docs/source/updates/updates.rst
@@ -357,6 +357,9 @@ If you do need the computational behaviour of a definition, it is now possible
 using local function definitions instead - see Section :ref:`sect-local-defs`
 below.
 
+Also, an alternative syntax ``let x := val in e`` is available.
+See Section :ref:`sect-let-bindings` for more info.
+
 ``auto``-implicits and Interfaces
 ---------------------------------