@@ -7,7 +7,7 @@ Theorem Proving
77Equality
88--------
99
10−allows propositional equalities to be declared, allowing theorems about
10+Idris allows propositional equalities to be declared, allowing theorems about
1111programs to be stated and proved. Equality is built in, but conceptually
1212has the following definition:
1313
@@ -301,7 +301,7 @@ anything:
301301 empty2 : Void
302302 empty2 = empty2
303303
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
305305the prompt with the ``:total`` command. We see that neither of the above
306306definitions is total:
307307
@@ -353,11 +353,10 @@ total, a function ``f`` must:
353353Directives and Compiler Flags for Totality
354354~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
355355
356−By default, allows all definitions, whether total or not. However, it is
357−desirable for functions to be total as far as possible, as this provides
358−a guarantee that they provide a result for all possible inputs, in
359−finite time. It is possible to make total functions a requirement,
360−either:
356+By default, Idris allows all well-typed definitions, whether total or not.
357+However, it is desirable for functions to be total as far as possible, as this
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, either:
361360
362361- By using the ``--total`` compiler flag.
363362
@@ -385,14 +384,13 @@ is total which is not. Do not rely on it for your proofs yet!
385384Hints for totality
386385~~~~~~~~~~~~~~~~~~
387386
388−In cases where you believe a program is total, but does not agree, it is
389−possible to give hints to the checker to give more detail for a
390−termination argument. The checker works by ensuring that all chains of
391−recursive calls eventually lead to one of the arguments decreasing
392−towards a base case, but sometimes this is hard to spot. For example,
393−the following definition cannot be checked as ``total`` because the
394−checker cannot decide that ``filter (<= x) xs`` will always be smaller
395−than ``(x :: xs)``:
387+In cases where you believe a program is total, but Idris does not agree, it is
388+possible to give hints to the checker to give more detail for a termination
389+argument. The checker works by ensuring that all chains of recursive calls
390+eventually lead to one of the arguments decreasing towards a base case, but
391+sometimes this is hard to spot. For example, the following definition cannot be
392+checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
393+will always be smaller than ``(x :: xs)``:
396394
397395.. code-block:: idris
398396