git.iko.soy/Idris-dev
on master help sign in
tidy up diagrams for example
commit19d6e296c26dd11666773d93caa911e3d9e30191 authorMartin Baker <git87465@martinb.com> dateThu 23 May 2019, 11:53 (7 years ago) parent75feef7
3 files changed+32−62
compare with master
unifiedsplit
docs/image/elabProofStateEx1_3.png docs/image/elabProofStateEx1_3.svg+28−58 docs/proofs/example1.rst+4−4
docs/image/elabProofStateEx1_3.png

Binary file not shown.

docs/image/elabProofStateEx1_3.svg+28−58
@@ -63,7 +63,8 @@
6363 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"
6464 xml:space="preserve"
6565 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
6768 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
6869 y="226.36218"
6970 x="401"
@@ -77,7 +78,8 @@
7778 y="198.36218"
7879 x="135"
7980 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
8183 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"
8284 y="198.36218"
8385 x="135"
@@ -91,7 +93,8 @@
9193 id="text4177"
9294 sodipodi:linespacing="125%"
9395 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
9598 sodipodi:role="line"
9699 id="tspan4179"
97100 x="393"
@@ -105,7 +108,8 @@
105108 y="197.36218"
106109 x="503"
107110 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
109113 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"
110114 y="197.36218"
111115 x="503"
@@ -119,7 +123,8 @@
119123 y="199.36218"
120124 x="247"
121125 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
123128 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"
124129 y="199.36218"
125130 x="247"
@@ -133,7 +138,8 @@
133138 x="134"
134139 y="205.3622"
135140 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" />
137143 <rect
138144 y="206.3622"
139145 x="234"
@@ -142,7 +148,8 @@
142148 id="rect4191"
143149 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"
144150 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" />
146153 <rect
147154 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"
148155 id="rect4195"
@@ -151,7 +158,8 @@
151158 x="497"
152159 y="205.3622"
153160 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" />
155163 <rect
156164 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"
157165 id="rect4197"
@@ -160,16 +168,8 @@
160168 x="389"
161169 y="237.3622"
162170 inkscape:export-xdpi="61.120499"
163− inkscape:export-ydpi="61.120499" />
164− <rect
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" />
171+ inkscape:export-ydpi="61.120499"
172+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png" />
173173 <rect
174174 y="205.3622"
175175 x="389"
@@ -178,7 +178,8 @@
178178 id="rect4201"
179179 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"
180180 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" />
182183 <text
183184 inkscape:export-ydpi="61.120499"
184185 inkscape:export-xdpi="61.120499"
@@ -187,7 +188,8 @@
187188 x="400"
188189 y="257.36218"
189190 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
191193 id="tspan4280"
192194 sodipodi:role="line"
193195 x="400"
@@ -201,7 +203,8 @@
201203 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"
202204 xml:space="preserve"
203205 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
205208 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
206209 y="225.36218"
207210 x="140"
@@ -215,47 +218,13 @@
215218 x="266"
216219 y="226.36218"
217220 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
219223 sodipodi:role="line"
220224 x="266"
221225 y="226.36218"
222226 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
223227 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" />
259228 <text
260229 inkscape:export-ydpi="61.120499"
261230 inkscape:export-xdpi="61.120499"
@@ -264,7 +233,8 @@
264233 x="510"
265234 y="226.36218"
266235 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
268238 id="tspan4176"
269239 sodipodi:role="line"
270240 x="510"
docs/proofs/example1.rst+4−4
@@ -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 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:
4444 - .. image:: ../image/elabLogicEx1_1.png
4545 :width: 126px
4646 :height: 33px
@@ -131,12 +131,12 @@ The following is a walkthough looking at the state after each tactic:
131131 * - Place a term into a hole, unifying its type
132132 - fill (Var \`{{x}})
133133
134− * - The state now looks like this:
134+ * - The state still looks like this:
135135 - .. image:: ../image/elabProofStateEx1_3.png
136136 :width: 312px
137− :height: 124px
137+ :height: 57px
138138
139− * - The logic now looks like this:
139+ * - and the logic like this:
140140 - .. image:: ../image/elabLogicEx1_3.png
141141 :width: 131px
142142 :height: 45px