@@ -33,22 +33,14 @@ declaration:
3333
3434.. code-block:: idris
3535
36− total
3736 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
3837
39−The ``total`` annotation means that we aim to write a function which
40−passes the totality checker; i.e. it will terminate on all possible
41−well-typed inputs. This is important for proofs, since it provides a
42−guarantee that the proof is valid in *all* cases, not just those for
43−which it happens to be well-defined.
44−
45−To create a template definition for the proof, press ``\d`` the
38+To create a template definition for the proof, press ``\d`` (or the
4639equivalent in your editor of choice) on the line with the type
4740declaration. You should see:
4841
4942.. code-block:: idris
5043
51− total
5244 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
5345 plus_commutes n m = ?plus_commutes_rhs
5446
@@ -59,7 +51,6 @@ should see:
5951
6052.. code-block:: idris
6153
62− total
6354 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
6455 plus_commutes Z m = ?plus_commutes_rhs_1
6556 plus_commutes (S k) m = ?plus_commutes_rhs_2
@@ -91,7 +82,6 @@ It is a good idea to give these slightly more meaningful names:
9182
9283.. code-block:: idris
9384
94− total
9585 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
9686 plus_commutes Z m = ?plus_commutes_Z
9787 plus_commutes (S k) m = ?plus_commutes_S
@@ -107,7 +97,6 @@ yields:
10797
10898 plus_commutes_Z : m = plus m 0
10999
110− total
111100 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
112101 plus_commutes Z m = plus_commutes_Z
113102 plus_commutes (S k) m = ?plus_commutes_S
@@ -280,7 +269,6 @@ state:
280269
281270.. code-block:: idris
282271
283− total
284272 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
285273 plus_commutes Z m = plus_commutes_Z
286274 plus_commutes (S k) m = ?plus_commutes_S
@@ -301,7 +289,6 @@ follows:
301289
302290.. code-block:: idris
303291
304− total
305292 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
306293 plus_commutes Z m = plus_commutes_Z
307294 plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
@@ -340,13 +327,21 @@ defined by matching on its first argument. The complete definition is:
340327
341328.. code-block:: idris
342329
330+ total
343331 plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
344332 plus_commutes_S k Z = Refl
345333 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
346334
347−All metavariables have now been solved, and ``plus_commutes`` has a
348−``total`` annotation, so we have completed the proof of commutativity of
349−addition on natural numbers.
335+All metavariables have now been solved,
336+
337+The ``total`` annotation means that we require the final function to
338+pass the totality checker; i.e. it will terminate on all possible
339+well-typed inputs. This is important for proofs, since it provides a
340+guarantee that the proof is valid in *all* cases, not just those for
341+which it happens to be well-defined.
342+
343+Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
344+proof of commutativity of addition on natural numbers.
350345
351346.. [1]
352347 Note that the left and right hand sides of the equality have been