git.iko.soy/Idris-dev
on master help sign in
update hole diagrams & remove reference to logic
commitdefab7386ffea030e4bd339e3a636129047c3908 authormartinbaker <git29f185@martinb.com> dateMon 1 Jul 2019, 08:05 (7 years ago) parent19d6e29
7 files changed+69−73
compare with master
unifiedsplit
docs/image/elabLogicEx1_1.png docs/image/elabLogicEx1_1.svg+25−23 docs/image/elabLogicEx1_2.png docs/image/elabLogicEx1_2.svg+15−18 docs/image/elabLogicEx1_3.png docs/image/elabLogicEx1_3.svg+19−22 docs/proofs/example1.rst+10−10
docs/image/elabLogicEx1_1.png

Binary file not shown.

docs/image/elabLogicEx1_1.svg+25−23
@@ -14,9 +14,9 @@
1414 viewBox="0 0 744.09448819 1052.3622047"
1515 id="svg2"
1616 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
1818 sodipodi:docname="elabLogicEx1_1.svg"
19− inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
19+ inkscape:export-filename="/home/mjb/Idris-dev/docs/image/elabLogicEx1_1.png"
2020 inkscape:export-xdpi="61.120499"
2121 inkscape:export-ydpi="61.120499">
2222 <defs
@@ -29,16 +29,16 @@
2929 inkscape:pageopacity="0.0"
3030 inkscape:pageshadow="2"
3131 inkscape:zoom="1"
32− inkscape:cx="425.25613"
32+ inkscape:cx="97.25613"
3333 inkscape:cy="593.17666"
3434 inkscape:document-units="px"
3535 inkscape:current-layer="layer1"
3636 showgrid="false"
37− inkscape:window-width="1131"
38− inkscape:window-height="1011"
39− inkscape:window-x="-4"
37+ inkscape:window-width="1920"
38+ inkscape:window-height="1015"
39+ inkscape:window-x="0"
4040 inkscape:window-y="0"
41− inkscape:window-maximized="0" />
41+ inkscape:window-maximized="1" />
4242 <metadata
4343 id="metadata7">
4444 <rdf:RDF>
@@ -47,7 +47,7 @@
4747 <dc:format>image/svg+xml</dc:format>
4848 <dc:type
4949 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
50− <dc:title></dc:title>
50+ <dc:title />
5151 </cc:Work>
5252 </rdf:RDF>
5353 </metadata>
@@ -56,15 +56,14 @@
5656 inkscape:groupmode="layer"
5757 id="layer1">
5858 <text
59− sodipodi:linespacing="125%"
6059 id="text4800"
6160 y="473.36218"
6261 x="205"
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"
62+ style="font-style:normal;font-weight:normal;line-height:0%;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"
6463 xml:space="preserve"
6564 inkscape:export-xdpi="61.120499"
6665 inkscape:export-ydpi="61.120499"><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'"
66+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
6867 y="473.36218"
6968 x="205"
7069 sodipodi:role="line"
@@ -73,25 +72,28 @@
7372 inkscape:export-ydpi="61.120499"
7473 inkscape:export-xdpi="61.120499"
7574 xml:space="preserve"
76− 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"
77− x="205"
78− y="500.36218"
79− id="text4178"
80− sodipodi:linespacing="125%"><tspan
75+ style="font-style:normal;font-weight:normal;line-height:0%;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"
76+ x="428.125"
77+ y="472.23718"
78+ id="text4178"><tspan
8179 id="tspan4180"
8280 sodipodi:role="line"
83− x="205"
84− y="500.36218"
85− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">hole_0 : pi_arg : Nat -&gt; Nat</tspan></text>
81+ x="428.125"
82+ y="472.23718"
83+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">hole_0 : pi_arg : Nat -&gt; Nat</tspan></text>
8684 <path
87− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none"
88− d="m 200,484.3622 185,-1"
85+ 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"
86+ d="m 423.125,456.2372 185,-1"
8987 id="path4182"
90− inkscape:connector-curvature="0" />
88+ inkscape:connector-curvature="0"
89+ inkscape:export-xdpi="61.120499"
90+ inkscape:export-ydpi="61.120499" />
9191 <path
9292 inkscape:connector-curvature="0"
9393 id="path4184"
9494 d="m 200,456.3622 185,-1"
95− 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" />
95+ 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"
96+ inkscape:export-xdpi="61.120499"
97+ inkscape:export-ydpi="61.120499" />
9698 </g>
9799</svg>
docs/image/elabLogicEx1_2.png

Binary file not shown.

docs/image/elabLogicEx1_2.svg+15−18
@@ -14,7 +14,7 @@
1414 viewBox="0 0 744.09448819 1052.3622047"
1515 id="svg2"
1616 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
1818 sodipodi:docname="elabLogicEx1_2.svg"
1919 inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
2020 inkscape:export-xdpi="61.120499"
@@ -56,15 +56,14 @@
5656 inkscape:groupmode="layer"
5757 id="layer1">
5858 <text
59− sodipodi:linespacing="125%"
6059 id="text4800"
6160 y="473.36218"
6261 x="205"
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"
62+ style="font-style:normal;font-weight:normal;line-height:0%;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"
6463 xml:space="preserve"
6564 inkscape:export-xdpi="61.120499"
6665 inkscape:export-ydpi="61.120499"><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'"
66+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
6867 y="473.36218"
6968 x="205"
7069 sodipodi:role="line"
@@ -73,19 +72,18 @@
7372 inkscape:export-ydpi="61.120499"
7473 inkscape:export-xdpi="61.120499"
7574 xml:space="preserve"
76− 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"
77− x="205"
78− y="500.36218"
79− id="text4178"
80− sodipodi:linespacing="125%"><tspan
75+ style="font-style:normal;font-weight:normal;line-height:0%;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"
76+ x="422.5"
77+ y="472.23718"
78+ id="text4178"><tspan
8179 id="tspan4180"
8280 sodipodi:role="line"
83− x="205"
84− y="500.36218"
85− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">hole_0 : (pi_arg : Nat) -&gt; Nat</tspan></text>
81+ x="422.5"
82+ y="472.23718"
83+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">hole_0 : (pi_arg : Nat) -&gt; Nat</tspan></text>
8684 <path
87− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none"
88− d="m 200,484.3622 185,-1"
85+ 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"
86+ d="m 417.5,456.2372 185,-1"
8987 id="path4182"
9088 inkscape:connector-curvature="0"
9189 inkscape:export-xdpi="61.120499"
@@ -101,15 +99,14 @@
10199 inkscape:export-ydpi="61.120499"
102100 inkscape:export-xdpi="61.120499"
103101 xml:space="preserve"
104− 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"
102+ style="font-style:normal;font-weight:normal;line-height:0%;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"
105103 x="229"
106104 y="447.36218"
107− id="text4147"
108− sodipodi:linespacing="125%"><tspan
105+ id="text4147"><tspan
109106 id="tspan4149"
110107 sodipodi:role="line"
111108 x="229"
112109 y="447.36218"
113− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">x : Nat</tspan></text>
110+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">x : Nat</tspan></text>
114111 </g>
115112</svg>
docs/image/elabLogicEx1_3.png

Binary file not shown.

docs/image/elabLogicEx1_3.svg+19−22
@@ -14,7 +14,7 @@
1414 viewBox="0 0 744.09448819 1052.3622047"
1515 id="svg2"
1616 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
1818 sodipodi:docname="elabLogicEx1_3.svg"
1919 inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
2020 inkscape:export-xdpi="61.120499"
@@ -34,11 +34,11 @@
3434 inkscape:document-units="px"
3535 inkscape:current-layer="layer1"
3636 showgrid="false"
37− inkscape:window-width="1175"
38− inkscape:window-height="1011"
39− inkscape:window-x="-4"
37+ inkscape:window-width="1920"
38+ inkscape:window-height="1015"
39+ inkscape:window-x="0"
4040 inkscape:window-y="0"
41− inkscape:window-maximized="0" />
41+ inkscape:window-maximized="1" />
4242 <metadata
4343 id="metadata7">
4444 <rdf:RDF>
@@ -56,15 +56,14 @@
5656 inkscape:groupmode="layer"
5757 id="layer1">
5858 <text
59− sodipodi:linespacing="125%"
6059 id="text4800"
6160 y="473.36218"
6261 x="205"
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"
62+ style="font-style:normal;font-weight:normal;line-height:0%;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"
6463 xml:space="preserve"
6564 inkscape:export-xdpi="61.120499"
6665 inkscape:export-ydpi="61.120499"><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'"
66+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
6867 y="473.36218"
6968 x="205"
7069 sodipodi:role="line"
@@ -73,19 +72,18 @@
7372 inkscape:export-ydpi="61.120499"
7473 inkscape:export-xdpi="61.120499"
7574 xml:space="preserve"
76− 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"
77− x="205"
78− y="500.36218"
79− id="text4178"
80− sodipodi:linespacing="125%"><tspan
75+ style="font-style:normal;font-weight:normal;line-height:0%;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"
76+ x="439.375"
77+ y="472.23718"
78+ id="text4178"><tspan
8179 id="tspan4180"
8280 sodipodi:role="line"
83− x="205"
84− y="500.36218"
85− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">hole_0 : (pi_arg : Nat) -&gt; Nat</tspan></text>
81+ x="439.375"
82+ y="472.23718"
83+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">hole_0 : (pi_arg : Nat) -&gt; Nat</tspan></text>
8684 <path
87− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none"
88− d="m 200,484.3622 185,-1"
85+ 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"
86+ d="m 434.375,456.2372 185,-1"
8987 id="path4182"
9088 inkscape:connector-curvature="0"
9189 inkscape:export-xdpi="61.120499"
@@ -101,15 +99,14 @@
10199 inkscape:export-ydpi="61.120499"
102100 inkscape:export-xdpi="61.120499"
103101 xml:space="preserve"
104− 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"
102+ style="font-style:normal;font-weight:normal;line-height:0%;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"
105103 x="229"
106104 y="447.36218"
107− id="text4147"
108− sodipodi:linespacing="125%"><tspan
105+ id="text4147"><tspan
109106 id="tspan4149"
110107 sodipodi:role="line"
111108 x="229"
112109 y="447.36218"
113− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">x : Nat</tspan></text>
110+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">x : Nat</tspan></text>
114111 </g>
115112</svg>
docs/proofs/example1.rst+10−10
@@ -40,10 +40,10 @@ 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. 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 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:
4444 - .. image:: ../image/elabLogicEx1_1.png
45− :width: 126px
46− :height: 33px
45+ :width: 277px
46+ :height: 15px
4747
4848 * - The term is:
4949 - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
@@ -88,10 +88,10 @@ The following is a walkthough looking at the state after each tactic:
8888 :width: 312px
8989 :height: 84px
9090
91− * - The logic now looks like this:
91+ * - The holes and what they depend on now looks like this:
9292 - .. image:: ../image/elabLogicEx1_2.png
93− :width: 126px
94− :height: 45px
93+ :width: 279px
94+ :height: 26px
9595
9696 * - The term now looks like this:
9797 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
@@ -136,10 +136,10 @@ The following is a walkthough looking at the state after each tactic:
136136 :width: 312px
137137 :height: 57px
138138
139− * - and the logic like this:
139+ * - The holes and what they depend on now looks like this:
140140 - .. image:: ../image/elabLogicEx1_3.png
141− :width: 131px
142− :height: 45px
141+ :width: 290px
142+ :height: 26px
143143
144144 * - The term now looks like this:
145145 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
@@ -189,7 +189,7 @@ The following is a walkthough looking at the state after each tactic:
189189 * - Substitute a guess into a hole.
190190 - solve
191191
192− * - The logic now looks like this:
192+ * - The holes and what they depend on now looks like this:
193193 - .. image:: ../image/elabLogicEx1_4.png
194194 :width: 131px
195195 :height: 14px