142f92f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix some pandoc conversion errors

commit142f92f38730d343d2d14841e2850447e5c7ef1a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 23 Mar 2015, 23:12 (12 years ago) parentdadfc86

1 file changed+10−10

compare with master

unifiedsplit

docs/proofs/patterns.rst+10−10

docs/proofs/patterns.rst+10−10

@@ -42,7 +42,7 @@ well-typed inputs. This is important for proofs, since it provides a

4242guarantee that the proof is valid in *all* cases, not just those for

4343which it happens to be well-defined.

4444

45−To create a template definition for the proof, press ``\backslashd`` the

45+To create a template definition for the proof, press ``\d`` the

4646equivalent in your editor of choice) on the line with the type

4747declaration. You should see:

4848

@@ -54,7 +54,7 @@ declaration. You should see:

5454

5555To prove this by induction on ``n``, as we sketched in Section

5656[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

5858should see:

5959

6060.. code-block:: idris

@@ -67,7 +67,7 @@ should see:

6767If we inspect the types of the newly created metavariables,

6868``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the

6969type 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

7171``plus_commutes_rhs_1`` shows:

7272

7373.. code-block:: idris

@@ -100,7 +100,7 @@ Base Case

100100---------

101101

102102We 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

104104yields:

105105

106106.. code-block:: idris

@@ -122,7 +122,7 @@ specific value for its *second argument* (in fact, the left hand side of

122122the equality has been reduced from ``plus 0 m``.) Again, we can prove

123123this by induction, this time on ``m``.

124124

125−First, create a template definition with ``\backslashd``:

125+First, create a template definition with ``\d``:

126126

127127.. code-block:: idris

128128

@@ -137,7 +137,7 @@ implciit, we will need to bring ``m`` into scope manually:

137137 plus_commutes_Z : m = plus m 0

138138 plus_commutes_Z {m} = ?plus_commutes_Z_rhs

139139

140−Now, case split on ``m`` with ``\backslashc``:

140+Now, case split on ``m`` with ``\c``:

141141

142142.. code-block:: idris

143143

@@ -154,7 +154,7 @@ which is easily proved by reflection:

154154 plus_commutes_Z_rhs_1 : 0 = 0

155155

156156For 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``.

158158This yields:

159159

160160.. code-block:: idris

@@ -260,7 +260,7 @@ In this case, inspecting the type of the hole gives:

260260 --------------------------------------

261261 plus_commutes_Z_rhs_2 : S k = S k

262262

263−Either way, we can use proof search (``\backslasho``) to complete the

263+Either way, we can use proof search (``\o``) to complete the

264264proof, giving:

265265

266266.. code-block:: idris

@@ -320,7 +320,7 @@ The good news is that ``m`` and ``k`` now appear in the correct order.

320320However, we still have to show that the successor symbol ``S`` can be

321321moved to the front in the right hand side of this equality. This

322322remaining 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:

324324

325325.. code-block:: idris

326326

@@ -328,7 +328,7 @@ begin by making a new top level lemma with ``\backslashl``. This gives:

328328

329329Unlike the previous case, ``k`` and ``m`` are not made implicit because

330330we 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``:

332332

333333.. code-block:: idris

334334