@@ -390,6 +390,12 @@ Totality
393+Sets explicitly to which extent pattern matching is terminating and/or
394+exhaustive. A ``partial`` pattern matching makes no assumption. A ``covering``
395+pattern matching ensures that pattern matching is exhaustive on its clauses.
396+Furthermore, a ``total`` pattern matching enforces both exhaustivity and
397+termination of the evaluation of its clauses.
393Implicit Coercion
399Implicit Coercion
394^^^^^^^^^^^^^^^^^
400^^^^^^^^^^^^^^^^^