git.iko.soy/Idris-dev
on master help sign in
update hole diagrams & remove reference to logic
defab73martinbaker
docs/image/elabLogicEx1_1.png
compare with master
unifiedsplit

Binary file not shown.

docs/image/elabLogicEx1_1.svg+25−23
@@ -14,9 +14,9 @@
14 viewBox="0 0 744.09448819 1052.3622047"
14 viewBox="0 0 744.09448819 1052.3622047"
15 id="svg2"
15 id="svg2"
16 version="1.1"
16 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18 sodipodi:docname="elabLogicEx1_1.svg"
18 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"
20 inkscape:export-xdpi="61.120499"
20 inkscape:export-xdpi="61.120499"
21 inkscape:export-ydpi="61.120499">
21 inkscape:export-ydpi="61.120499">
22 <defs
22 <defs
@@ -29,16 +29,16 @@
29 inkscape:pageopacity="0.0"
29 inkscape:pageopacity="0.0"
30 inkscape:pageshadow="2"
30 inkscape:pageshadow="2"
31 inkscape:zoom="1"
31 inkscape:zoom="1"
32− inkscape:cx="425.25613"
32+ inkscape:cx="97.25613"
33 inkscape:cy="593.17666"
33 inkscape:cy="593.17666"
34 inkscape:document-units="px"
34 inkscape:document-units="px"
35 inkscape:current-layer="layer1"
35 inkscape:current-layer="layer1"
36 showgrid="false"
36 showgrid="false"
37− inkscape:window-width="1131"
37+ inkscape:window-width="1920"
38− inkscape:window-height="1011"
38+ inkscape:window-height="1015"
39− inkscape:window-x="-4"
39+ inkscape:window-x="0"
40 inkscape:window-y="0"
40 inkscape:window-y="0"
41− inkscape:window-maximized="0" />
41+ inkscape:window-maximized="1" />
42 <metadata
42 <metadata
43 id="metadata7">
43 id="metadata7">
44 <rdf:RDF>
44 <rdf:RDF>
@@ -47,7 +47,7 @@
47 <dc:format>image/svg+xml</dc:format>
47 <dc:format>image/svg+xml</dc:format>
48 <dc:type
48 <dc:type
49 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
49 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
50− <dc:title></dc:title>
50+ <dc:title />
51 </cc:Work>
51 </cc:Work>
52 </rdf:RDF>
52 </rdf:RDF>
53 </metadata>
53 </metadata>
@@ -56,15 +56,14 @@
56 inkscape:groupmode="layer"
56 inkscape:groupmode="layer"
57 id="layer1">
57 id="layer1">
58 <text
58 <text
59− sodipodi:linespacing="125%"
60 id="text4800"
59 id="text4800"
61 y="473.36218"
60 y="473.36218"
62 x="205"
61 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"
64 xml:space="preserve"
63 xml:space="preserve"
65 inkscape:export-xdpi="61.120499"
64 inkscape:export-xdpi="61.120499"
66 inkscape:export-ydpi="61.120499"><tspan
65 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'"
68 y="473.36218"
67 y="473.36218"
69 x="205"
68 x="205"
70 sodipodi:role="line"
69 sodipodi:role="line"
@@ -73,25 +72,28 @@
73 inkscape:export-ydpi="61.120499"
72 inkscape:export-ydpi="61.120499"
74 inkscape:export-xdpi="61.120499"
73 inkscape:export-xdpi="61.120499"
75 xml:space="preserve"
74 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"
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"
77− x="205"
76+ x="428.125"
78− y="500.36218"
77+ y="472.23718"
79− id="text4178"
78+ id="text4178"><tspan
80− sodipodi:linespacing="125%"><tspan
81 id="tspan4180"
79 id="tspan4180"
82 sodipodi:role="line"
80 sodipodi:role="line"
83− x="205"
81+ x="428.125"
84− y="500.36218"
82+ y="472.23718"
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>
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>
86 <path
84 <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"
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"
88− d="m 200,484.3622 185,-1"
86+ d="m 423.125,456.2372 185,-1"
89 id="path4182"
87 id="path4182"
90− inkscape:connector-curvature="0" />
88+ inkscape:connector-curvature="0"
89+ inkscape:export-xdpi="61.120499"
90+ inkscape:export-ydpi="61.120499" />
91 <path
91 <path
92 inkscape:connector-curvature="0"
92 inkscape:connector-curvature="0"
93 id="path4184"
93 id="path4184"
94 d="m 200,456.3622 185,-1"
94 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" />
96 </g>
98 </g>
97</svg>
99</svg>
docs/image/elabLogicEx1_2.png

Binary file not shown.

docs/image/elabLogicEx1_2.svg+15−18
@@ -14,7 +14,7 @@
14 viewBox="0 0 744.09448819 1052.3622047"
14 viewBox="0 0 744.09448819 1052.3622047"
15 id="svg2"
15 id="svg2"
16 version="1.1"
16 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18 sodipodi:docname="elabLogicEx1_2.svg"
18 sodipodi:docname="elabLogicEx1_2.svg"
19 inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
19 inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
20 inkscape:export-xdpi="61.120499"
20 inkscape:export-xdpi="61.120499"
@@ -56,15 +56,14 @@
56 inkscape:groupmode="layer"
56 inkscape:groupmode="layer"
57 id="layer1">
57 id="layer1">
58 <text
58 <text
59− sodipodi:linespacing="125%"
60 id="text4800"
59 id="text4800"
61 y="473.36218"
60 y="473.36218"
62 x="205"
61 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"
64 xml:space="preserve"
63 xml:space="preserve"
65 inkscape:export-xdpi="61.120499"
64 inkscape:export-xdpi="61.120499"
66 inkscape:export-ydpi="61.120499"><tspan
65 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'"
68 y="473.36218"
67 y="473.36218"
69 x="205"
68 x="205"
70 sodipodi:role="line"
69 sodipodi:role="line"
@@ -73,19 +72,18 @@
73 inkscape:export-ydpi="61.120499"
72 inkscape:export-ydpi="61.120499"
74 inkscape:export-xdpi="61.120499"
73 inkscape:export-xdpi="61.120499"
75 xml:space="preserve"
74 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"
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"
77− x="205"
76+ x="422.5"
78− y="500.36218"
77+ y="472.23718"
79− id="text4178"
78+ id="text4178"><tspan
80− sodipodi:linespacing="125%"><tspan
81 id="tspan4180"
79 id="tspan4180"
82 sodipodi:role="line"
80 sodipodi:role="line"
83− x="205"
81+ x="422.5"
84− y="500.36218"
82+ y="472.23718"
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>
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>
86 <path
84 <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"
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"
88− d="m 200,484.3622 185,-1"
86+ d="m 417.5,456.2372 185,-1"
89 id="path4182"
87 id="path4182"
90 inkscape:connector-curvature="0"
88 inkscape:connector-curvature="0"
91 inkscape:export-xdpi="61.120499"
89 inkscape:export-xdpi="61.120499"
@@ -101,15 +99,14 @@
101 inkscape:export-ydpi="61.120499"
99 inkscape:export-ydpi="61.120499"
102 inkscape:export-xdpi="61.120499"
100 inkscape:export-xdpi="61.120499"
103 xml:space="preserve"
101 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"
105 x="229"
103 x="229"
106 y="447.36218"
104 y="447.36218"
107− id="text4147"
105+ id="text4147"><tspan
108− sodipodi:linespacing="125%"><tspan
109 id="tspan4149"
106 id="tspan4149"
110 sodipodi:role="line"
107 sodipodi:role="line"
111 x="229"
108 x="229"
112 y="447.36218"
109 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>
114 </g>
111 </g>
115</svg>
112</svg>
docs/image/elabLogicEx1_3.png

Binary file not shown.

docs/image/elabLogicEx1_3.svg+19−22
@@ -14,7 +14,7 @@
14 viewBox="0 0 744.09448819 1052.3622047"
14 viewBox="0 0 744.09448819 1052.3622047"
15 id="svg2"
15 id="svg2"
16 version="1.1"
16 version="1.1"
17− inkscape:version="0.91 r13725"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18 sodipodi:docname="elabLogicEx1_3.svg"
18 sodipodi:docname="elabLogicEx1_3.svg"
19 inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
19 inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"
20 inkscape:export-xdpi="61.120499"
20 inkscape:export-xdpi="61.120499"
@@ -34,11 +34,11 @@
34 inkscape:document-units="px"
34 inkscape:document-units="px"
35 inkscape:current-layer="layer1"
35 inkscape:current-layer="layer1"
36 showgrid="false"
36 showgrid="false"
37− inkscape:window-width="1175"
37+ inkscape:window-width="1920"
38− inkscape:window-height="1011"
38+ inkscape:window-height="1015"
39− inkscape:window-x="-4"
39+ inkscape:window-x="0"
40 inkscape:window-y="0"
40 inkscape:window-y="0"
41− inkscape:window-maximized="0" />
41+ inkscape:window-maximized="1" />
42 <metadata
42 <metadata
43 id="metadata7">
43 id="metadata7">
44 <rdf:RDF>
44 <rdf:RDF>
@@ -56,15 +56,14 @@
56 inkscape:groupmode="layer"
56 inkscape:groupmode="layer"
57 id="layer1">
57 id="layer1">
58 <text
58 <text
59− sodipodi:linespacing="125%"
60 id="text4800"
59 id="text4800"
61 y="473.36218"
60 y="473.36218"
62 x="205"
61 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"
64 xml:space="preserve"
63 xml:space="preserve"
65 inkscape:export-xdpi="61.120499"
64 inkscape:export-xdpi="61.120499"
66 inkscape:export-ydpi="61.120499"><tspan
65 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'"
68 y="473.36218"
67 y="473.36218"
69 x="205"
68 x="205"
70 sodipodi:role="line"
69 sodipodi:role="line"
@@ -73,19 +72,18 @@
73 inkscape:export-ydpi="61.120499"
72 inkscape:export-ydpi="61.120499"
74 inkscape:export-xdpi="61.120499"
73 inkscape:export-xdpi="61.120499"
75 xml:space="preserve"
74 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"
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"
77− x="205"
76+ x="439.375"
78− y="500.36218"
77+ y="472.23718"
79− id="text4178"
78+ id="text4178"><tspan
80− sodipodi:linespacing="125%"><tspan
81 id="tspan4180"
79 id="tspan4180"
82 sodipodi:role="line"
80 sodipodi:role="line"
83− x="205"
81+ x="439.375"
84− y="500.36218"
82+ y="472.23718"
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>
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>
86 <path
84 <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"
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"
88− d="m 200,484.3622 185,-1"
86+ d="m 434.375,456.2372 185,-1"
89 id="path4182"
87 id="path4182"
90 inkscape:connector-curvature="0"
88 inkscape:connector-curvature="0"
91 inkscape:export-xdpi="61.120499"
89 inkscape:export-xdpi="61.120499"
@@ -101,15 +99,14 @@
101 inkscape:export-ydpi="61.120499"
99 inkscape:export-ydpi="61.120499"
102 inkscape:export-xdpi="61.120499"
100 inkscape:export-xdpi="61.120499"
103 xml:space="preserve"
101 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"
105 x="229"
103 x="229"
106 y="447.36218"
104 y="447.36218"
107− id="text4147"
105+ id="text4147"><tspan
108− sodipodi:linespacing="125%"><tspan
109 id="tspan4149"
106 id="tspan4149"
110 sodipodi:role="line"
107 sodipodi:role="line"
111 x="229"
108 x="229"
112 y="447.36218"
109 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>
114 </g>
111 </g>
115</svg>
112</svg>
docs/proofs/example1.rst+10−10
@@ -40,10 +40,10 @@ 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. 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:
44 - .. image:: ../image/elabLogicEx1_1.png
44 - .. image:: ../image/elabLogicEx1_1.png
45− :width: 126px
45+ :width: 277px
46− :height: 33px
46+ :height: 15px
47
47
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}
@@ -88,10 +88,10 @@ The following is a walkthough looking at the state after each tactic:
88 :width: 312px
88 :width: 312px
89 :height: 84px
89 :height: 84px
90
90
91− * - The logic now looks like this:
91+ * - The holes and what they depend on now looks like this:
92 - .. image:: ../image/elabLogicEx1_2.png
92 - .. image:: ../image/elabLogicEx1_2.png
93− :width: 126px
93+ :width: 279px
94− :height: 45px
94+ :height: 26px
95
95
96 * - The term now looks like this:
96 * - The term now looks like this:
97 - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
97 - ?{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:
136 :width: 312px
136 :width: 312px
137 :height: 57px
137 :height: 57px
138
138
139− * - and the logic like this:
139+ * - The holes and what they depend on now looks like this:
140 - .. image:: ../image/elabLogicEx1_3.png
140 - .. image:: ../image/elabLogicEx1_3.png
141− :width: 131px
141+ :width: 290px
142− :height: 45px
142+ :height: 26px
143
143
144 * - The term now looks like this:
144 * - The term now looks like this:
145 - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
145 - ?{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:
189 * - Substitute a guess into a hole.
189 * - Substitute a guess into a hole.
190 - solve
190 - solve
191
191
192− * - The logic now looks like this:
192+ * - The holes and what they depend on now looks like this:
193 - .. image:: ../image/elabLogicEx1_4.png
193 - .. image:: ../image/elabLogicEx1_4.png
194 :width: 131px
194 :width: 131px
195 :height: 14px
195 :height: 14px