@@ -46,7 +46,7 @@ declaration. You should see:
46 plus_commutes n m = ?plus_commutes_rhs
46 plus_commutes n m = ?plus_commutes_rhs
48To prove this by induction on ``n``, as we sketched in Section
48To prove this by induction on ``n``, as we sketched in Section
49−[sect:induction], we begin with a case split on ``n`` (press
49+:ref:`sect-inductive`, we begin with a case split on ``n`` (press
50``\c`` with the cursor over the ``n`` in the definition.) You
50``\c`` with the cursor over the ``n`` in the definition.) You
51should see:
51should see:
@@ -334,7 +334,7 @@ defined by matching on its first argument. The complete definition is:
334 plus_commutes_S k Z = Refl
334 plus_commutes_S k Z = Refl
335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
337−All metavariables have now been solved,
337+All metavariables have now been solved.
339The ``total`` annotation means that we require the final function to
339The ``total`` annotation means that we require the final function to
340pass the totality checker; i.e. it will terminate on all possible
340pass the totality checker; i.e. it will terminate on all possible