@@ -46,7 +46,7 @@ declaration. You should see:
4646 plus_commutes n m = ?plus_commutes_rhs
4747
4848To 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
5050``\c`` with the cursor over the ``n`` in the definition.) You
5151should see:
5252
@@ -334,7 +334,7 @@ defined by matching on its first argument. The complete definition is:
334334 plus_commutes_S k Z = Refl
335335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
336336
337−All metavariables have now been solved,
337+All metavariables have now been solved.
338338
339339The ``total`` annotation means that we require the final function to
340340pass the totality checker; i.e. it will terminate on all possible