@@ -469,6 +469,16 @@ It is a matter of taste whether you want to do this — sometimes it can
469469help document a function by making the purpose of an argument more
470470clear.
471471
472+Furthermore, ``{}`` can be used to pattern match on the left hand side, i.e.
473+``{var = pat}`` gets an implicit variable and attempts to pattern match on "pat";
474+For example :
475+
476+.. code-block:: idris
477+
478+ isEmpty : Vect n a -> Bool
479+ isEmpty {n = Z} _ = True
480+ isEmpty {n = S k} _ = False
481+
472482“``using``” notation
473483--------------------
474484