@@ -7,7 +7,7 @@ Theorem Proving
10−allows propositional equalities to be declared, allowing theorems about
10+Idris allows propositional equalities to be declared, allowing theorems about
11programs to be stated and proved. Equality is built in, but conceptually
11programs to be stated and proved. Equality is built in, but conceptually
12has the following definition:
12has the following definition:
@@ -301,7 +301,7 @@ anything:
301 empty2 : Void
301 empty2 : Void
302 empty2 = empty2
302 empty2 = empty2
304−Internally, checks every definition for totality, and we can check at
304+Internally, Idris checks every definition for totality, and we can check at
305the prompt with the ``:total`` command. We see that neither of the above
305the prompt with the ``:total`` command. We see that neither of the above
306definitions is total:
306definitions is total:
@@ -353,11 +353,10 @@ total, a function ``f`` must:
353Directives and Compiler Flags for Totality
353Directives and Compiler Flags for Totality
354~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
356−By default, allows all definitions, whether total or not. However, it is
356+By default, Idris allows all well-typed definitions, whether total or not.
357−desirable for functions to be total as far as possible, as this provides
357+However, it is desirable for functions to be total as far as possible, as this
358−a guarantee that they provide a result for all possible inputs, in
358+provides a guarantee that they provide a result for all possible inputs, in
359−finite time. It is possible to make total functions a requirement,
359+finite time. It is possible to make total functions a requirement, either:
362- By using the ``--total`` compiler flag.
361- By using the ``--total`` compiler flag.
@@ -385,14 +384,13 @@ is total which is not. Do not rely on it for your proofs yet!
385Hints for totality
384Hints for totality
386~~~~~~~~~~~~~~~~~~
385~~~~~~~~~~~~~~~~~~
388−In cases where you believe a program is total, but does not agree, it is
387+In cases where you believe a program is total, but Idris does not agree, it is
389−possible to give hints to the checker to give more detail for a
388+possible to give hints to the checker to give more detail for a termination
390−termination argument. The checker works by ensuring that all chains of
389+argument. The checker works by ensuring that all chains of recursive calls
391−recursive calls eventually lead to one of the arguments decreasing
390+eventually lead to one of the arguments decreasing towards a base case, but
392−towards a base case, but sometimes this is hard to spot. For example,
391+sometimes this is hard to spot. For example, the following definition cannot be
393−the following definition cannot be checked as ``total`` because the
394−checker cannot decide that ``filter (<= x) xs`` will always be smaller
392+checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
395−than ``(x :: xs)``:
393+will always be smaller than ``(x :: xs)``:
397.. code-block:: idris
395.. code-block:: idris