@@ -40,7 +40,7 @@ The following is a walkthough looking at the state after each tactic:
4040 :width: 310px
4141 :height: 115px
4242
43− * - This table also shows the holes and what they depend on. The aim is to illustrate the tactics by analogy with proofs, as a line with the premises above it and the conclusion below it. The conclusion is the hole we are trying to fill and the premises may be sub-goals:
43+ * - This table shows the hole types and what they depend on. The aim is to illustrate the types by analogy with proofs, as a line with the premises above it and the conclusion below it.
4444 - .. image:: ../image/elabLogicEx1_1.png
4545 :width: 277px
4646 :height: 15px
@@ -48,11 +48,7 @@ The following is a walkthough looking at the state after each tactic:
4848 * - The term is:
4949 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
5050
51− * - getEnv
52−
53− getGoal
54−
55− getHoles
51+ * - It is possible to read the state from the script by calling getEnv, getGoal and getHoles. To show the results I hacked this: `my code`_.
5652
5753 - .. code-block:: idris
5854
@@ -88,7 +84,7 @@ The following is a walkthough looking at the state after each tactic:
8884 :width: 312px
8985 :height: 84px
9086
91− * - The holes and what they depend on now looks like this:
87+ * - The hole types now looks like this:
9288 - .. image:: ../image/elabLogicEx1_2.png
9389 :width: 279px
9490 :height: 26px
@@ -96,11 +92,7 @@ The following is a walkthough looking at the state after each tactic:
9692 * - The term now looks like this:
9793 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
9894
99− * - getEnv
100−
101− getGoal
102−
103− getHoles
95+ * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
10496
10597 - .. code-block:: idris
10698
@@ -136,7 +128,7 @@ The following is a walkthough looking at the state after each tactic:
136128 :width: 312px
137129 :height: 57px
138130
139− * - The holes and what they depend on now looks like this:
131+ * - The hole types now looks like this:
140132 - .. image:: ../image/elabLogicEx1_3.png
141133 :width: 290px
142134 :height: 26px
@@ -144,11 +136,7 @@ The following is a walkthough looking at the state after each tactic:
144136 * - The term now looks like this:
145137 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
146138
147− * - getEnv
148−
149− getGoal
150−
151− getHoles
139+ * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
152140
153141 - .. code-block:: idris
154142
@@ -189,7 +177,7 @@ The following is a walkthough looking at the state after each tactic:
189177 * - Substitute a guess into a hole.
190178 - solve
191179
192− * - The holes and what they depend on now looks like this:
180+ * - The hole types now looks like this:
193181 - .. image:: ../image/elabLogicEx1_4.png
194182 :width: 131px
195183 :height: 14px
@@ -246,3 +234,6 @@ The following is a walkthough looking at the state after each tactic:
246234 }
247235 }
248236 }
237+
238+.. target-notes::
239+.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr