@@ -116,12 +116,17 @@ We can do the same for the reduction behaviour of plus on successors:
116116Even for trival theorems like these, the proofs are a little tricky to
117117construct in one go. When things get even slightly more complicated, it
118118becomes too much to think about to construct proofs in this ‘batch
119−mode’. therefore provides an interactive proof mode.
119+mode’.
120+
121+Idris provides interactive editing capabilities, which can help with
122+building proofs. For more details on building proofs interactively in
123+an editor, see :ref:`proofs-index`. In the rest of this section, we discuss
124+Idris's interactive proof mode.
120125
121126Interactive theorem proving
122127---------------------------
123128
124−Instead of writing the proof in one go, we can use ’s interactive proof
129+Instead of writing the proof in one go, we can use Idris’s interactive proof
125130mode. To do this, we write the general *structure* of the proof, and use
126131the interactive mode to complete the details. We’ll be constructing the
127132proof by *induction*, so we write the cases for ``Z`` and ``S``, with a