@@ -42,7 +42,7 @@ well-typed inputs. This is important for proofs, since it provides a
42guarantee that the proof is valid in *all* cases, not just those for
42guarantee that the proof is valid in *all* cases, not just those for
43which it happens to be well-defined.
43which it happens to be well-defined.
45−To create a template definition for the proof, press ``\backslashd`` the
45+To create a template definition for the proof, press ``\d`` the
46equivalent in your editor of choice) on the line with the type
46equivalent in your editor of choice) on the line with the type
47declaration. You should see:
47declaration. You should see:
@@ -54,7 +54,7 @@ declaration. You should see:
55To prove this by induction on ``n``, as we sketched in Section
55To prove this by induction on ``n``, as we sketched in Section
56[sect:induction], we begin with a case split on ``n`` (press
56[sect:induction], we begin with a case split on ``n`` (press
57−``\backslashc`` with the cursor over the ``n`` in the definition.) You
57+``\c`` with the cursor over the ``n`` in the definition.) You
58should see:
58should see:
60.. code-block:: idris
60.. code-block:: idris
@@ -67,7 +67,7 @@ should see:
67If we inspect the types of the newly created metavariables,
67If we inspect the types of the newly created metavariables,
68``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the
68``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the
69type of each reflects that ``n`` has been refined to ``Z`` and ``S k``
69type of each reflects that ``n`` has been refined to ``Z`` and ``S k``
70−in each respective case. Pressing ``\backslasht`` over
70+in each respective case. Pressing ``\t`` over
71``plus_commutes_rhs_1`` shows:
71``plus_commutes_rhs_1`` shows:
73.. code-block:: idris
73.. code-block:: idris
@@ -100,7 +100,7 @@ Base Case
102We can create a separate lemma for the base case interactively, by
102We can create a separate lemma for the base case interactively, by
103−pressing ``\backslashl`` with the cursor over ``plus_commutes_Z``. This
103+pressing ``\l`` with the cursor over ``plus_commutes_Z``. This
106.. code-block:: idris
106.. code-block:: idris
@@ -122,7 +122,7 @@ specific value for its *second argument* (in fact, the left hand side of
122the equality has been reduced from ``plus 0 m``.) Again, we can prove
122the equality has been reduced from ``plus 0 m``.) Again, we can prove
123this by induction, this time on ``m``.
123this by induction, this time on ``m``.
125−First, create a template definition with ``\backslashd``:
125+First, create a template definition with ``\d``:
127.. code-block:: idris
127.. code-block:: idris
@@ -137,7 +137,7 @@ implciit, we will need to bring ``m`` into scope manually:
137 plus_commutes_Z : m = plus m 0
137 plus_commutes_Z : m = plus m 0
138 plus_commutes_Z {m} = ?plus_commutes_Z_rhs
138 plus_commutes_Z {m} = ?plus_commutes_Z_rhs
140−Now, case split on ``m`` with ``\backslashc``:
140+Now, case split on ``m`` with ``\c``:
142.. code-block:: idris
142.. code-block:: idris
@@ -154,7 +154,7 @@ which is easily proved by reflection:
154 plus_commutes_Z_rhs_1 : 0 = 0
154 plus_commutes_Z_rhs_1 : 0 = 0
156For such trivial proofs, we can let write the proof automatically by
156For such trivial proofs, we can let write the proof automatically by
157−pressing ``\backslasho`` with the cursor over ``plus_commutes_Z_rhs_1``.
157+pressing ``\o`` with the cursor over ``plus_commutes_Z_rhs_1``.
158This yields:
158This yields:
160.. code-block:: idris
160.. code-block:: idris
@@ -260,7 +260,7 @@ In this case, inspecting the type of the hole gives:
260 --------------------------------------
260 --------------------------------------
261 plus_commutes_Z_rhs_2 : S k = S k
261 plus_commutes_Z_rhs_2 : S k = S k
263−Either way, we can use proof search (``\backslasho``) to complete the
263+Either way, we can use proof search (``\o``) to complete the
264proof, giving:
264proof, giving:
266.. code-block:: idris
266.. code-block:: idris
@@ -320,7 +320,7 @@ The good news is that ``m`` and ``k`` now appear in the correct order.
320However, we still have to show that the successor symbol ``S`` can be
320However, we still have to show that the successor symbol ``S`` can be
321moved to the front in the right hand side of this equality. This
321moved to the front in the right hand side of this equality. This
322remaining lemma takes a similar form to the ``plus_commutes_Z``; we
322remaining lemma takes a similar form to the ``plus_commutes_Z``; we
323−begin by making a new top level lemma with ``\backslashl``. This gives:
323+begin by making a new top level lemma with ``\l``. This gives:
325.. code-block:: idris
325.. code-block:: idris
@@ -328,7 +328,7 @@ begin by making a new top level lemma with ``\backslashl``. This gives:
329Unlike the previous case, ``k`` and ``m`` are not made implicit because
329Unlike the previous case, ``k`` and ``m`` are not made implicit because
330we cannot in general infer arguments to a function from its result.
330we cannot in general infer arguments to a function from its result.
331−Again, we make a template definition with ``\backslashd``:
331+Again, we make a template definition with ``\d``:
333.. code-block:: idris
333.. code-block:: idris