git.iko.soy/Idris-dev
on master help sign in
add diagram for attack
c891750martinbaker
docs/image/attack.pngnew file
compare with master
unifiedsplit

Binary file not shown.

docs/image/attack.svgnew file+199
@@ -0,0 +1,199 @@
1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2+<!-- Created with Inkscape (http://www.inkscape.org/) -->
3+
4+<svg
5+ xmlns:dc="http://purl.org/dc/elements/1.1/"
6+ xmlns:cc="http://creativecommons.org/ns#"
7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
8+ xmlns:svg="http://www.w3.org/2000/svg"
9+ xmlns="http://www.w3.org/2000/svg"
10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
12+ width="210mm"
13+ height="297mm"
14+ viewBox="0 0 210 297"
15+ version="1.1"
16+ id="svg8"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18+ sodipodi:docname="attack.svg">
19+ <defs
20+ id="defs2">
21+ <marker
22+ inkscape:stockid="Arrow1Mend"
23+ orient="auto"
24+ refY="0.0"
25+ refX="0.0"
26+ id="marker890"
27+ style="overflow:visible;"
28+ inkscape:isstock="true">
29+ <path
30+ id="path888"
31+ 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+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
33+ transform="scale(0.4) rotate(180) translate(10,0)" />
34+ </marker>
35+ <marker
36+ inkscape:isstock="true"
37+ style="overflow:visible;"
38+ id="marker838"
39+ refX="0.0"
40+ refY="0.0"
41+ orient="auto"
42+ inkscape:stockid="Arrow1Mend"
43+ inkscape:collect="always">
44+ <path
45+ transform="scale(0.4) rotate(180) translate(10,0)"
46+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
47+ 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 "
48+ id="path836" />
49+ </marker>
50+ <marker
51+ inkscape:stockid="Arrow1Mend"
52+ orient="auto"
53+ refY="0.0"
54+ refX="0.0"
55+ id="Arrow1Mend"
56+ style="overflow:visible;"
57+ inkscape:isstock="true"
58+ inkscape:collect="always">
59+ <path
60+ id="path4529"
61+ 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 "
62+ style="fill-rule:evenodd;stroke:#ff0000;stroke-width:1pt;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
63+ transform="scale(0.4) rotate(180) translate(10,0)" />
64+ </marker>
65+ </defs>
66+ <sodipodi:namedview
67+ id="base"
68+ pagecolor="#ffffff"
69+ bordercolor="#666666"
70+ borderopacity="1.0"
71+ inkscape:pageopacity="0.0"
72+ inkscape:pageshadow="2"
73+ inkscape:zoom="1"
74+ inkscape:cx="313.5"
75+ inkscape:cy="696.5"
76+ inkscape:document-units="mm"
77+ inkscape:current-layer="layer1"
78+ showgrid="false"
79+ inkscape:window-width="1920"
80+ inkscape:window-height="1015"
81+ inkscape:window-x="0"
82+ inkscape:window-y="0"
83+ inkscape:window-maximized="1" />
84+ <metadata
85+ id="metadata5">
86+ <rdf:RDF>
87+ <cc:Work
88+ rdf:about="">
89+ <dc:format>image/svg+xml</dc:format>
90+ <dc:type
91+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
92+ <dc:title />
93+ </cc:Work>
94+ </rdf:RDF>
95+ </metadata>
96+ <g
97+ inkscape:label="Layer 1"
98+ inkscape:groupmode="layer"
99+ id="layer1">
100+ <rect
101+ style="fill:#ffff00;fill-opacity:1;stroke-width:0.26458332"
102+ id="rect22"
103+ width="28.839582"
104+ height="6.0854182"
105+ x="66.67498"
106+ y="114.4375"
107+ inkscape:export-xdpi="61.120499"
108+ inkscape:export-ydpi="61.120499" />
109+ <text
110+ xml:space="preserve"
111+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
112+ x="65.352081"
113+ y="105.17709"
114+ id="text12"
115+ inkscape:export-xdpi="61.120499"
116+ inkscape:export-ydpi="61.120499"><tspan
117+ sodipodi:role="line"
118+ x="65.352081"
119+ y="105.17709"
120+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
121+ id="tspan847">?h ∶ t1→t2 . f h</tspan></text>
122+ <text
123+ id="text16"
124+ y="118.67083"
125+ x="56.356247"
126+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
127+ xml:space="preserve"
128+ inkscape:export-xdpi="61.120499"
129+ inkscape:export-ydpi="61.120499"><tspan
130+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
131+ y="118.67083"
132+ x="56.356247"
133+ id="tspan14"
134+ sodipodi:role="line">?h ≈ (?h' ∶ t1→t2 . h')∶ t1→t2 . f h</tspan></text>
135+ <text
136+ id="text20"
137+ y="110.99791"
138+ x="82.814583"
139+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
140+ xml:space="preserve"
141+ inkscape:export-xdpi="61.120499"
142+ inkscape:export-ydpi="61.120499"><tspan
143+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
144+ y="110.99791"
145+ x="82.814583"
146+ id="tspan18"
147+ sodipodi:role="line">attack</tspan></text>
148+ <path
149+ style="fill:none;stroke:#ff0000;stroke-width:0.5291667;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
150+ d="m 80.668481,106.30075 -0.0032,7.57492"
151+ id="path4518"
152+ inkscape:connector-curvature="0"
153+ sodipodi:nodetypes="cc"
154+ inkscape:export-xdpi="61.120499"
155+ inkscape:export-ydpi="61.120499" />
156+ <text
157+ inkscape:export-ydpi="61.120499"
158+ inkscape:export-xdpi="61.120499"
159+ xml:space="preserve"
160+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
161+ x="63.235413"
162+ y="94.85833"
163+ id="text832"><tspan
164+ sodipodi:role="line"
165+ id="tspan830"
166+ x="63.235413"
167+ y="94.85833"
168+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">focus</tspan></text>
169+ <path
170+ inkscape:export-ydpi="61.120499"
171+ inkscape:export-xdpi="61.120499"
172+ sodipodi:nodetypes="cc"
173+ inkscape:connector-curvature="0"
174+ id="path834"
175+ d="m 66.645564,94.659084 -0.0032,5.458256"
176+ style="fill:none;stroke:#0000ff;stroke-width:0.5291667;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker838)" />
177+ <text
178+ id="text884"
179+ y="110.23682"
180+ x="61.94511"
181+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
182+ xml:space="preserve"
183+ inkscape:export-xdpi="61.120499"
184+ inkscape:export-ydpi="61.120499"><tspan
185+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332"
186+ y="110.23682"
187+ x="61.94511"
188+ id="tspan882"
189+ sodipodi:role="line">focus</tspan></text>
190+ <path
191+ style="fill:none;stroke:#0000ff;stroke-width:0.5291667;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker890)"
192+ d="m 66.67818,108.97924 -0.0032,5.45826"
193+ id="path886"
194+ inkscape:connector-curvature="0"
195+ sodipodi:nodetypes="cc"
196+ inkscape:export-xdpi="61.120499"
197+ inkscape:export-ydpi="61.120499" />
198+ </g>
199+</svg>
docs/proofs/primitive.rst+7−2
@@ -144,9 +144,14 @@ Primitive Operators
144 unfocus : TTName -> Elab ()
144 unfocus : TTName -> Elab ()
145
145
146 * - attack
146 * - attack
147− - Convert a hole to make it suitable for bindings - that is, transform it such that it has the form
147+ - Convert a hole to make it suitable for bindings.
148+
149+
150+ .. image:: ../image/attack.png
151+ :width: 152px
152+ :height: 70px
153+ :alt: diagram illustrating attack tactic
148
154
149− `?h : t . h` as opposed to `?h : t . f h`.
150
155
151 The binding tactics require that a hole be directly under its binding, or else the scopes of the generated terms won't make sense. This tactic creates a new hole of the proper form, and points the old hole at it.
156 The binding tactics require that a hole be directly under its binding, or else the scopes of the generated terms won't make sense. This tactic creates a new hole of the proper form, and points the old hole at it.
152
157