git.iko.soy/Idris-dev
on master help sign in
corrections to identity example
810528dmartinbaker
docs/proofs/example1.rst+10−19
compare with master
unifiedsplit
@@ -40,7 +40,7 @@ The following is a walkthough looking at the state after each tactic:
40 :width: 310px
40 :width: 310px
41 :height: 115px
41 :height: 115px
42
42
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.
44 - .. image:: ../image/elabLogicEx1_1.png
44 - .. image:: ../image/elabLogicEx1_1.png
45 :width: 277px
45 :width: 277px
46 :height: 15px
46 :height: 15px
@@ -48,11 +48,7 @@ The following is a walkthough looking at the state after each tactic:
48 * - The term is:
48 * - The term is:
49 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
49 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
50
50
51− * - getEnv
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`_.
52−
53− getGoal
54−
55− getHoles
56
52
57 - .. code-block:: idris
53 - .. code-block:: idris
58
54
@@ -88,7 +84,7 @@ The following is a walkthough looking at the state after each tactic:
88 :width: 312px
84 :width: 312px
89 :height: 84px
85 :height: 84px
90
86
91− * - The holes and what they depend on now looks like this:
87+ * - The hole types now looks like this:
92 - .. image:: ../image/elabLogicEx1_2.png
88 - .. image:: ../image/elabLogicEx1_2.png
93 :width: 279px
89 :width: 279px
94 :height: 26px
90 :height: 26px
@@ -96,11 +92,7 @@ The following is a walkthough looking at the state after each tactic:
96 * - The term now looks like this:
92 * - The term now looks like this:
97 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
93 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
98
94
99− * - getEnv
95+ * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
100−
101− getGoal
102−
103− getHoles
104
96
105 - .. code-block:: idris
97 - .. code-block:: idris
106
98
@@ -136,7 +128,7 @@ The following is a walkthough looking at the state after each tactic:
136 :width: 312px
128 :width: 312px
137 :height: 57px
129 :height: 57px
138
130
139− * - The holes and what they depend on now looks like this:
131+ * - The hole types now looks like this:
140 - .. image:: ../image/elabLogicEx1_3.png
132 - .. image:: ../image/elabLogicEx1_3.png
141 :width: 290px
133 :width: 290px
142 :height: 26px
134 :height: 26px
@@ -144,11 +136,7 @@ The following is a walkthough looking at the state after each tactic:
144 * - The term now looks like this:
136 * - The term now looks like this:
145 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
137 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
146
138
147− * - getEnv
139+ * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
148−
149− getGoal
150−
151− getHoles
152
140
153 - .. code-block:: idris
141 - .. code-block:: idris
154
142
@@ -189,7 +177,7 @@ The following is a walkthough looking at the state after each tactic:
189 * - Substitute a guess into a hole.
177 * - Substitute a guess into a hole.
190 - solve
178 - solve
191
179
192− * - The holes and what they depend on now looks like this:
180+ * - The hole types now looks like this:
193 - .. image:: ../image/elabLogicEx1_4.png
181 - .. image:: ../image/elabLogicEx1_4.png
194 :width: 131px
182 :width: 131px
195 :height: 14px
183 :height: 14px
@@ -246,3 +234,6 @@ The following is a walkthough looking at the state after each tactic:
246 }
234 }
247 }
235 }
248 }
236 }
237+
238+.. target-notes::
239+.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr