@@ -116,12 +116,17 @@ We can do the same for the reduction behaviour of plus on successors:
116Even for trival theorems like these, the proofs are a little tricky to
116Even for trival theorems like these, the proofs are a little tricky to
117construct in one go. When things get even slightly more complicated, it
117construct in one go. When things get even slightly more complicated, it
118becomes too much to think about to construct proofs in this ‘batch
118becomes too much to think about to construct proofs in this ‘batch
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
119−mode’. therefore provides an interactive proof mode.
124+Idris's interactive proof mode.
121Interactive theorem proving
126Interactive theorem proving
122---------------------------
127---------------------------
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
125mode. To do this, we write the general *structure* of the proof, and use
130mode. To do this, we write the general *structure* of the proof, and use
126the interactive mode to complete the details. We’ll be constructing the
131the interactive mode to complete the details. We’ll be constructing the
127proof by *induction*, so we write the cases for ``Z`` and ``S``, with a
132proof by *induction*, so we write the cases for ``Z`` and ``S``, with a