+ <para>Warning: the format for a path for a <emphasis role="bold">match</emphasis> … <emphasis role="bold">with</emphasis>
+ expression is restricted to: <emphasis role="bold">match</emphasis> &path;
+ <emphasis role="bold">with</emphasis>
+ <emphasis role="bold">[</emphasis>
+ <emphasis role="bold">_</emphasis>
+ <emphasis role="bold">⇒</emphasis>
+ &path;
+ <emphasis role="bold">|</emphasis> …
+ <emphasis role="bold">|</emphasis>
+ <emphasis role="bold">_</emphasis>
+ <emphasis role="bold">⇒</emphasis>
+ &path;
+ <emphasis role="bold">]</emphasis>
+ Its semantics is the following: the n-th
+ "<emphasis role="bold">_</emphasis>
+ <emphasis role="bold">⇒</emphasis>
+ &path;" branch is matched against the n-th constructor of the
+ inductive data type. The head λ-abstractions of &path; are matched
+ against the corresponding constructor arguments.
+ </para>