git.iko.soy/Idris-dev
on master help sign in
tidy up diagrams for example
19d6e29Martin Baker
docs/image/elabProofStateEx1_3.png
compare with master
unifiedsplit

Binary file not shown.

docs/image/elabProofStateEx1_3.svg+28−58
@@ -63,7 +63,8 @@
63 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
63 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
64 xml:space="preserve"
64 xml:space="preserve"
65 inkscape:export-xdpi="61.120499"
65 inkscape:export-xdpi="61.120499"
66− inkscape:export-ydpi="61.120499"><tspan
66+ inkscape:export-ydpi="61.120499"
67+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
67 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
68 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
68 y="226.36218"
69 y="226.36218"
69 x="401"
70 x="401"
@@ -77,7 +78,8 @@
77 y="198.36218"
78 y="198.36218"
78 x="135"
79 x="135"
79 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
80 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
80− xml:space="preserve"><tspan
81+ xml:space="preserve"
82+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
81 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
83 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
82 y="198.36218"
84 y="198.36218"
83 x="135"
85 x="135"
@@ -91,7 +93,8 @@
91 id="text4177"
93 id="text4177"
92 sodipodi:linespacing="125%"
94 sodipodi:linespacing="125%"
93 inkscape:export-xdpi="61.120499"
95 inkscape:export-xdpi="61.120499"
94− inkscape:export-ydpi="61.120499"><tspan
96+ inkscape:export-ydpi="61.120499"
97+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
95 sodipodi:role="line"
98 sodipodi:role="line"
96 id="tspan4179"
99 id="tspan4179"
97 x="393"
100 x="393"
@@ -105,7 +108,8 @@
105 y="197.36218"
108 y="197.36218"
106 x="503"
109 x="503"
107 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
110 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
108− xml:space="preserve"><tspan
111+ xml:space="preserve"
112+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
109 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
113 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
110 y="197.36218"
114 y="197.36218"
111 x="503"
115 x="503"
@@ -119,7 +123,8 @@
119 y="199.36218"
123 y="199.36218"
120 x="247"
124 x="247"
121 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
125 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
122− xml:space="preserve"><tspan
126+ xml:space="preserve"
127+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
123 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
128 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;fill-opacity:1"
124 y="199.36218"
129 y="199.36218"
125 x="247"
130 x="247"
@@ -133,7 +138,8 @@
133 x="134"
138 x="134"
134 y="205.3622"
139 y="205.3622"
135 inkscape:export-xdpi="61.120499"
140 inkscape:export-xdpi="61.120499"
136− inkscape:export-ydpi="61.120499" />
141+ inkscape:export-ydpi="61.120499"
142+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png" />
137 <rect
143 <rect
138 y="206.3622"
144 y="206.3622"
139 x="234"
145 x="234"
@@ -142,7 +148,8 @@
142 id="rect4191"
148 id="rect4191"
143 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
149 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
144 inkscape:export-xdpi="61.120499"
150 inkscape:export-xdpi="61.120499"
145− inkscape:export-ydpi="61.120499" />
151+ inkscape:export-ydpi="61.120499"
152+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png" />
146 <rect
153 <rect
147 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
154 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
148 id="rect4195"
155 id="rect4195"
@@ -151,7 +158,8 @@
151 x="497"
158 x="497"
152 y="205.3622"
159 y="205.3622"
153 inkscape:export-xdpi="61.120499"
160 inkscape:export-xdpi="61.120499"
154− inkscape:export-ydpi="61.120499" />
161+ inkscape:export-ydpi="61.120499"
162+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png" />
155 <rect
163 <rect
156 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
164 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
157 id="rect4197"
165 id="rect4197"
@@ -160,16 +168,8 @@
160 x="389"
168 x="389"
161 y="237.3622"
169 y="237.3622"
162 inkscape:export-xdpi="61.120499"
170 inkscape:export-xdpi="61.120499"
163− inkscape:export-ydpi="61.120499" />
171+ inkscape:export-ydpi="61.120499"
164− <rect
172+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png" />
165− y="269.36218"
166− x="389"
167− height="32"
168− width="95"
169− id="rect4199"
170− style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
171− inkscape:export-xdpi="61.120499"
172− inkscape:export-ydpi="61.120499" />
173 <rect
173 <rect
174 y="205.3622"
174 y="205.3622"
175 x="389"
175 x="389"
@@ -178,7 +178,8 @@
178 id="rect4201"
178 id="rect4201"
179 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
179 style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
180 inkscape:export-xdpi="61.120499"
180 inkscape:export-xdpi="61.120499"
181− inkscape:export-ydpi="61.120499" />
181+ inkscape:export-ydpi="61.120499"
182+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png" />
182 <text
183 <text
183 inkscape:export-ydpi="61.120499"
184 inkscape:export-ydpi="61.120499"
184 inkscape:export-xdpi="61.120499"
185 inkscape:export-xdpi="61.120499"
@@ -187,7 +188,8 @@
187 x="400"
188 x="400"
188 y="257.36218"
189 y="257.36218"
189 id="text4276"
190 id="text4276"
190− sodipodi:linespacing="125%"><tspan
191+ sodipodi:linespacing="125%"
192+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
191 id="tspan4280"
193 id="tspan4280"
192 sodipodi:role="line"
194 sodipodi:role="line"
193 x="400"
195 x="400"
@@ -201,7 +203,8 @@
201 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
203 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
202 xml:space="preserve"
204 xml:space="preserve"
203 inkscape:export-xdpi="61.120499"
205 inkscape:export-xdpi="61.120499"
204− inkscape:export-ydpi="61.120499"><tspan
206+ inkscape:export-ydpi="61.120499"
207+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
205 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
208 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
206 y="225.36218"
209 y="225.36218"
207 x="140"
210 x="140"
@@ -215,47 +218,13 @@
215 x="266"
218 x="266"
216 y="226.36218"
219 y="226.36218"
217 id="text4786"
220 id="text4786"
218− sodipodi:linespacing="125%"><tspan
221+ sodipodi:linespacing="125%"
222+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
219 sodipodi:role="line"
223 sodipodi:role="line"
220 x="266"
224 x="266"
221 y="226.36218"
225 y="226.36218"
222 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
226 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
223 id="tspan4790">(hole_2 , Nat)</tspan></text>
227 id="tspan4790">(hole_2 , Nat)</tspan></text>
224− <path
225− inkscape:connector-curvature="0"
226− id="path4798"
227− d="m 298,236.3622 9,98"
228− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
229− sodipodi:nodetypes="cc"
230− inkscape:export-xdpi="61.120499"
231− inkscape:export-ydpi="61.120499" />
232− <text
233− sodipodi:linespacing="125%"
234− id="text4800"
235− y="350.36218"
236− x="404"
237− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
238− xml:space="preserve"
239− inkscape:export-xdpi="61.120499"
240− inkscape:export-ydpi="61.120499"><tspan
241− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
242− y="350.36218"
243− x="404"
244− sodipodi:role="line"
245− id="tspan4802">machine chosen</tspan><tspan
246− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
247− y="369.11218"
248− x="404"
249− sodipodi:role="line"
250− id="tspan4812">names for the holes</tspan></text>
251− <path
252− sodipodi:nodetypes="cc"
253− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
254− d="m 432,265.3622 8,68"
255− id="path4804"
256− inkscape:connector-curvature="0"
257− inkscape:export-xdpi="61.120499"
258− inkscape:export-ydpi="61.120499" />
259 <text
228 <text
260 inkscape:export-ydpi="61.120499"
229 inkscape:export-ydpi="61.120499"
261 inkscape:export-xdpi="61.120499"
230 inkscape:export-xdpi="61.120499"
@@ -264,7 +233,8 @@
264 x="510"
233 x="510"
265 y="226.36218"
234 y="226.36218"
266 id="text4174"
235 id="text4174"
267− sodipodi:linespacing="125%"><tspan
236+ sodipodi:linespacing="125%"
237+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"><tspan
268 id="tspan4176"
238 id="tspan4176"
269 sodipodi:role="line"
239 sodipodi:role="line"
270 x="510"
240 x="510"
docs/proofs/example1.rst+4−4
@@ -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 logic at each stage:
43+ * - This table also shows the logic at each stage. 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:
44 - .. image:: ../image/elabLogicEx1_1.png
44 - .. image:: ../image/elabLogicEx1_1.png
45 :width: 126px
45 :width: 126px
46 :height: 33px
46 :height: 33px
@@ -131,12 +131,12 @@ The following is a walkthough looking at the state after each tactic:
131 * - Place a term into a hole, unifying its type
131 * - Place a term into a hole, unifying its type
132 - fill (Var \`{{x}})
132 - fill (Var \`{{x}})
133
133
134− * - The state now looks like this:
134+ * - The state still looks like this:
135 - .. image:: ../image/elabProofStateEx1_3.png
135 - .. image:: ../image/elabProofStateEx1_3.png
136 :width: 312px
136 :width: 312px
137− :height: 124px
137+ :height: 57px
138
138
139− * - The logic now looks like this:
139+ * - and the logic like this:
140 - .. image:: ../image/elabLogicEx1_3.png
140 - .. image:: ../image/elabLogicEx1_3.png
141 :width: 131px
141 :width: 131px
142 :height: 45px
142 :height: 45px