git.iko.soy/Idris-dev
on master help sign in
corrections to identity example
8f8303emartinbaker
docs/image/tree.png
compare with master
unifiedsplit

Binary file not shown.

docs/image/tree.svg+109−77
@@ -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="tree.svg">
18 sodipodi:docname="tree.svg">
19 <defs
19 <defs
20 id="defs4">
20 id="defs4">
@@ -32,21 +32,6 @@
32 d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
32 d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
33 id="path5206" />
33 id="path5206" />
34 </marker>
34 </marker>
35− <marker
36− inkscape:stockid="Arrow1Mend"
37− orient="auto"
38− refY="0.0"
39− refX="0.0"
40− id="Arrow1Mend"
41− style="overflow:visible;"
42− inkscape:isstock="true"
43− inkscape:collect="always">
44− <path
45− id="path4179"
46− d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
47− style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
48− transform="scale(0.4) rotate(180) translate(10,0)" />
49− </marker>
50 </defs>
35 </defs>
51 <sodipodi:namedview
36 <sodipodi:namedview
52 id="base"
37 id="base"
@@ -57,13 +42,13 @@
57 inkscape:pageshadow="2"
42 inkscape:pageshadow="2"
58 inkscape:zoom="1"
43 inkscape:zoom="1"
59 inkscape:cx="383.03443"
44 inkscape:cx="383.03443"
60− inkscape:cy="520"
45+ inkscape:cy="690.88799"
61 inkscape:document-units="px"
46 inkscape:document-units="px"
62 inkscape:current-layer="layer1"
47 inkscape:current-layer="layer1"
63 showgrid="false"
48 showgrid="false"
64− inkscape:window-width="1406"
49+ inkscape:window-width="1129"
65− inkscape:window-height="1011"
50+ inkscape:window-height="730"
66− inkscape:window-x="-4"
51+ inkscape:window-x="671"
67 inkscape:window-y="0"
52 inkscape:window-y="0"
68 inkscape:window-maximized="0" />
53 inkscape:window-maximized="0" />
69 <metadata
54 <metadata
@@ -74,7 +59,7 @@
74 <dc:format>image/svg+xml</dc:format>
59 <dc:format>image/svg+xml</dc:format>
75 <dc:type
60 <dc:type
76 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
61 rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
77− <dc:title></dc:title>
62+ <dc:title />
78 </cc:Work>
63 </cc:Work>
79 </rdf:RDF>
64 </rdf:RDF>
80 </metadata>
65 </metadata>
@@ -84,97 +69,144 @@
84 id="layer1">
69 id="layer1">
85 <text
70 <text
86 xml:space="preserve"
71 xml:space="preserve"
87− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
72+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
88− x="221"
73+ x="348.5"
89− y="433.36221"
74+ y="334.92474"
90 id="text4136"
75 id="text4136"
91− sodipodi:linespacing="125%"
92 inkscape:export-xdpi="61.120499"
76 inkscape:export-xdpi="61.120499"
93 inkscape:export-ydpi="61.120499"><tspan
77 inkscape:export-ydpi="61.120499"><tspan
94 sodipodi:role="line"
78 sodipodi:role="line"
95 id="tspan4138"
79 id="tspan4138"
96− x="221"
80+ x="348.5"
97− y="433.36221"
81+ y="334.92474"
98− 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">λ n:t1 . h:t2</tspan></text>
82+ 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';fill:#0000ff;fill-opacity:1">{hole2} :Nat-&gt;Nat</tspan></text>
99 <text
83 <text
100− xml:space="preserve"
101− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
102− x="260"
103− y="366.36221"
104− id="text4144"
105− sodipodi:linespacing="125%"
106− inkscape:export-xdpi="61.120499"
107− inkscape:export-ydpi="61.120499"><tspan
108− sodipodi:role="line"
109− id="tspan4146"
110− x="260"
111− y="366.36221"
112− 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">x</tspan></text>
113− <path
114− 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"
115− d="m 268,373.3622 13,43"
116− id="path4150"
117− inkscape:connector-curvature="0"
118− sodipodi:nodetypes="cc"
119− inkscape:export-xdpi="61.120499"
120− inkscape:export-ydpi="61.120499" />
121− <text
122− sodipodi:linespacing="125%"
123 id="text4152"
84 id="text4152"
124− y="466.36221"
85+ y="364.17471"
125− x="161"
86+ x="380.375"
126− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
87+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
127 xml:space="preserve"
88 xml:space="preserve"
128 inkscape:export-xdpi="61.120499"
89 inkscape:export-xdpi="61.120499"
129 inkscape:export-ydpi="61.120499"><tspan
90 inkscape:export-ydpi="61.120499"><tspan
130− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"
91+ 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';fill:#000000;fill-opacity:1"
131− y="466.36221"
92+ y="364.17471"
132− x="161"
93+ x="380.375"
133 id="tspan4154"
94 id="tspan4154"
134 sodipodi:role="line">intro `{{x}}</tspan></text>
95 sodipodi:role="line">intro `{{x}}</tspan></text>
135 <text
96 <text
136 xml:space="preserve"
97 xml:space="preserve"
137− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
98+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
138− x="322"
99+ x="381.0625"
139− y="468.36221"
100+ y="470.23721"
140 id="text4156"
101 id="text4156"
141− sodipodi:linespacing="125%"
142 inkscape:export-xdpi="61.120499"
102 inkscape:export-xdpi="61.120499"
143 inkscape:export-ydpi="61.120499"><tspan
103 inkscape:export-ydpi="61.120499"><tspan
144 sodipodi:role="line"
104 sodipodi:role="line"
145 id="tspan4158"
105 id="tspan4158"
146− x="322"
106+ x="381.0625"
147− y="468.36221"
107+ y="470.23721"
148− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1">solve</tspan></text>
108+ 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';fill:#000000;fill-opacity:1">solve</tspan></text>
149 <text
109 <text
150− sodipodi:linespacing="125%"
151 id="text4160"
110 id="text4160"
152− y="325.36221"
111+ y="414.42471"
153− x="224"
112+ x="380.5625"
154− style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
113+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
155 xml:space="preserve"
114 xml:space="preserve"
156 inkscape:export-xdpi="61.120499"
115 inkscape:export-xdpi="61.120499"
157 inkscape:export-ydpi="61.120499"><tspan
116 inkscape:export-ydpi="61.120499"><tspan
158− style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"
117+ 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';fill:#000000;fill-opacity:1"
159− y="325.36221"
118+ y="414.42471"
160− x="224"
119+ x="380.5625"
161 id="tspan4162"
120 id="tspan4162"
162 sodipodi:role="line">fill (Var `{{x}})</tspan></text>
121 sodipodi:role="line">fill (Var `{{x}})</tspan></text>
163 <path
122 <path
164− sodipodi:nodetypes="cc"
123+ style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)"
124+ d="m 371.4375,343.4872 0.875,29.125"
125+ id="path5202"
165 inkscape:connector-curvature="0"
126 inkscape:connector-curvature="0"
166− id="path4164"
127+ sodipodi:nodetypes="cc"
167− d="m 179,448.3622 76,-117"
168− style="fill:none;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
169 inkscape:export-xdpi="61.120499"
128 inkscape:export-xdpi="61.120499"
170 inkscape:export-ydpi="61.120499" />
129 inkscape:export-ydpi="61.120499" />
130+ <path
131+ inkscape:export-ydpi="61.120499"
132+ inkscape:export-xdpi="61.120499"
133+ sodipodi:nodetypes="cc"
134+ inkscape:connector-curvature="0"
135+ id="path89"
136+ d="m 371.4375,395.9872 0.875,29.125"
137+ style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)" />
171 <path
138 <path
172 style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)"
139 style="fill:#0000ff;fill-rule:evenodd;stroke:#0000ff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5204)"
173− d="m 273,330.3622 59,121"
140+ d="m 371.4375,450.3622 0.875,29.125"
174− id="path5202"
141+ id="path91"
175 inkscape:connector-curvature="0"
142 inkscape:connector-curvature="0"
176 sodipodi:nodetypes="cc"
143 sodipodi:nodetypes="cc"
177 inkscape:export-xdpi="61.120499"
144 inkscape:export-xdpi="61.120499"
178 inkscape:export-ydpi="61.120499" />
145 inkscape:export-ydpi="61.120499" />
146+ <text
147+ inkscape:export-ydpi="61.120499"
148+ inkscape:export-xdpi="61.120499"
149+ id="text95"
150+ y="332.11224"
151+ x="295.0625"
152+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
153+ xml:space="preserve"><tspan
154+ 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';fill:#ff0000;fill-opacity:1"
155+ y="332.11224"
156+ x="295.0625"
157+ id="tspan93"
158+ sodipodi:role="line">state</tspan></text>
159+ <text
160+ xml:space="preserve"
161+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
162+ x="295.0625"
163+ y="386.48724"
164+ id="text99"
165+ inkscape:export-xdpi="61.120499"
166+ inkscape:export-ydpi="61.120499"><tspan
167+ sodipodi:role="line"
168+ id="tspan97"
169+ x="295.0625"
170+ y="386.48724"
171+ 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';fill:#ff0000;fill-opacity:1">state</tspan></text>
172+ <text
173+ inkscape:export-ydpi="61.120499"
174+ inkscape:export-xdpi="61.120499"
175+ id="text103"
176+ y="444.61224"
177+ x="295.0625"
178+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
179+ xml:space="preserve"><tspan
180+ 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';fill:#ff0000;fill-opacity:1"
181+ y="444.61224"
182+ x="295.0625"
183+ id="tspan101"
184+ sodipodi:role="line">state</tspan></text>
185+ <text
186+ inkscape:export-ydpi="61.120499"
187+ inkscape:export-xdpi="61.120499"
188+ id="text3796"
189+ y="389.29974"
190+ x="345.6875"
191+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
192+ xml:space="preserve"><tspan
193+ 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';fill:#0000ff;fill-opacity:1"
194+ y="389.29974"
195+ x="345.6875"
196+ id="tspan3794"
197+ sodipodi:role="line">λ x:Nat . ? {hole 2}</tspan></text>
198+ <text
199+ xml:space="preserve"
200+ style="font-style:normal;font-weight:normal;line-height:0%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
201+ x="344.75"
202+ y="442.73724"
203+ id="text3800"
204+ inkscape:export-xdpi="61.120499"
205+ inkscape:export-ydpi="61.120499"><tspan
206+ sodipodi:role="line"
207+ id="tspan3798"
208+ x="344.75"
209+ y="442.73724"
210+ 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';fill:#0000ff;fill-opacity:1">λ x:Nat . x</tspan></text>
179 </g>
211 </g>
180</svg>
212</svg>
docs/proofs/example1.rst+2−2
@@ -20,8 +20,8 @@ Elaborator Reflection - Identity Example
20
20
21 As a first approximation, the state consists of a term with holes in it, an indicator of which hole is focused, a queue of the next holes to focus on, and miscellaneous information like a source of fresh names. The intro tactic modifies this state, replacing the focused hole with a lambda and focusing on the lambda's body.
21 As a first approximation, the state consists of a term with holes in it, an indicator of which hole is focused, a queue of the next holes to focus on, and miscellaneous information like a source of fresh names. The intro tactic modifies this state, replacing the focused hole with a lambda and focusing on the lambda's body.
22 - .. image:: ../image/tree.png
22 - .. image:: ../image/tree.png
23− :width: 133px
23+ :width: 119px
24− :height: 106px
24+ :height: 109px
25
25
26The following is a walkthough looking at the state after each tactic:
26The following is a walkthough looking at the state after each tactic:
27
27