@@ -233,7 +233,7 @@ possible to give hints to the checker to give more detail for a termination
233argument. The checker works by ensuring that all chains of recursive calls
233argument. The checker works by ensuring that all chains of recursive calls
234eventually lead to one of the arguments decreasing towards a base case, but
234eventually lead to one of the arguments decreasing towards a base case, but
235sometimes this is hard to spot. For example, the following definition cannot be
235sometimes this is hard to spot. For example, the following definition cannot be
236−checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
236+checked as ``total`` because the checker cannot decide that ``filter (< x) xs``
237will always be smaller than ``(x :: xs)``:
237will always be smaller than ``(x :: xs)``:
239.. code-block:: idris
239.. code-block:: idris