@@ -469,6 +469,16 @@ It is a matter of taste whether you want to do this — sometimes it can
469help document a function by making the purpose of an argument more
469help document a function by making the purpose of an argument more
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";
476+.. code-block:: idris
478+ isEmpty : Vect n a -> Bool
479+ isEmpty {n = Z} _ = True
480+ isEmpty {n = S k} _ = False
472“``using``” notation
482“``using``” notation
473--------------------
483--------------------