git.iko.soy/Idris-dev
on master help sign in
changes to generatingData.rst
231d842Martin Baker
docs/image/generateFunction.pngnew file
compare with master
unifiedsplit

Binary file not shown.

docs/image/generateFunction.svgnew file+588
@@ -0,0 +1,588 @@
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 744.09448819 1052.3622047"
15+ id="svg2"
16+ version="1.1"
17+ inkscape:version="0.91 r13725"
18+ sodipodi:docname="generateFunction.svg">
19+ <defs
20+ id="defs4">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker4348"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow2Mend">
29+ <path
30+ transform="scale(0.6) rotate(180) translate(0,0)"
31+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
32+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
33+ id="path4350" />
34+ </marker>
35+ <marker
36+ inkscape:isstock="true"
37+ style="overflow:visible;"
38+ id="marker7147"
39+ refX="0.0"
40+ refY="0.0"
41+ orient="auto"
42+ inkscape:stockid="Arrow2Mend">
43+ <path
44+ transform="scale(0.6) rotate(180) translate(0,0)"
45+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
46+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
47+ id="path7149" />
48+ </marker>
49+ <marker
50+ inkscape:stockid="Arrow2Mend"
51+ orient="auto"
52+ refY="0.0"
53+ refX="0.0"
54+ id="marker6819"
55+ style="overflow:visible;"
56+ inkscape:isstock="true"
57+ inkscape:collect="always">
58+ <path
59+ id="path6821"
60+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
61+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
62+ transform="scale(0.6) rotate(180) translate(0,0)" />
63+ </marker>
64+ <marker
65+ inkscape:isstock="true"
66+ style="overflow:visible;"
67+ id="marker6325"
68+ refX="0.0"
69+ refY="0.0"
70+ orient="auto"
71+ inkscape:stockid="Arrow2Mend">
72+ <path
73+ transform="scale(0.6) rotate(180) translate(0,0)"
74+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
75+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
76+ id="path6327" />
77+ </marker>
78+ <marker
79+ inkscape:stockid="Arrow2Mend"
80+ orient="auto"
81+ refY="0.0"
82+ refX="0.0"
83+ id="marker5163"
84+ style="overflow:visible;"
85+ inkscape:isstock="true">
86+ <path
87+ id="path5165"
88+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
89+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
90+ transform="scale(0.6) rotate(180) translate(0,0)" />
91+ </marker>
92+ <marker
93+ inkscape:isstock="true"
94+ style="overflow:visible;"
95+ id="marker5133"
96+ refX="0.0"
97+ refY="0.0"
98+ orient="auto"
99+ inkscape:stockid="Arrow2Mend"
100+ inkscape:collect="always">
101+ <path
102+ transform="scale(0.6) rotate(180) translate(0,0)"
103+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
104+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
105+ id="path5135" />
106+ </marker>
107+ <marker
108+ inkscape:stockid="Arrow2Mend"
109+ orient="auto"
110+ refY="0.0"
111+ refX="0.0"
112+ id="Arrow2Mend"
113+ style="overflow:visible;"
114+ inkscape:isstock="true"
115+ inkscape:collect="always">
116+ <path
117+ id="path4183"
118+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
119+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
120+ transform="scale(0.6) rotate(180) translate(0,0)" />
121+ </marker>
122+ </defs>
123+ <sodipodi:namedview
124+ id="base"
125+ pagecolor="#ffffff"
126+ bordercolor="#666666"
127+ borderopacity="1.0"
128+ inkscape:pageopacity="0.0"
129+ inkscape:pageshadow="2"
130+ inkscape:zoom="1"
131+ inkscape:cx="380.92935"
132+ inkscape:cy="520"
133+ inkscape:document-units="px"
134+ inkscape:current-layer="layer1"
135+ showgrid="false"
136+ inkscape:window-width="1212"
137+ inkscape:window-height="1011"
138+ inkscape:window-x="0"
139+ inkscape:window-y="0"
140+ inkscape:window-maximized="0" />
141+ <metadata
142+ id="metadata7">
143+ <rdf:RDF>
144+ <cc:Work
145+ rdf:about="">
146+ <dc:format>image/svg+xml</dc:format>
147+ <dc:type
148+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
149+ <dc:title />
150+ </cc:Work>
151+ </rdf:RDF>
152+ </metadata>
153+ <g
154+ inkscape:label="Layer 1"
155+ inkscape:groupmode="layer"
156+ id="layer1">
157+ <rect
158+ style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
159+ id="rect4136"
160+ width="201"
161+ height="69"
162+ x="116"
163+ y="203.3622"
164+ inkscape:export-xdpi="61.120499"
165+ inkscape:export-ydpi="61.120499" />
166+ <rect
167+ y="322.36218"
168+ x="113"
169+ height="69"
170+ width="201"
171+ id="rect4138"
172+ 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"
173+ inkscape:export-xdpi="61.120499"
174+ inkscape:export-ydpi="61.120499" />
175+ <rect
176+ y="202.3622"
177+ x="381"
178+ height="69"
179+ width="201"
180+ id="rect4140"
181+ style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
182+ inkscape:export-xdpi="61.120499"
183+ inkscape:export-ydpi="61.120499" />
184+ <text
185+ xml:space="preserve"
186+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
187+ x="125"
188+ y="227.3622"
189+ id="text4142"
190+ sodipodi:linespacing="125%"
191+ inkscape:export-xdpi="61.120499"
192+ inkscape:export-ydpi="61.120499"><tspan
193+ sodipodi:role="line"
194+ id="tspan4144"
195+ x="125"
196+ y="227.3622">declareType</tspan></text>
197+ <text
198+ sodipodi:linespacing="125%"
199+ id="text4146"
200+ y="225.3622"
201+ x="389"
202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
203+ xml:space="preserve"
204+ inkscape:export-xdpi="61.120499"
205+ inkscape:export-ydpi="61.120499"><tspan
206+ y="225.3622"
207+ x="389"
208+ id="tspan4148"
209+ sodipodi:role="line">defineFunction</tspan></text>
210+ <path
211+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5133)"
212+ d="m 190,271.3622 0,48"
213+ id="path4150"
214+ inkscape:connector-curvature="0"
215+ inkscape:export-xdpi="61.120499"
216+ inkscape:export-ydpi="61.120499" />
217+ <text
218+ sodipodi:linespacing="125%"
219+ id="text5074"
220+ y="295.36218"
221+ x="201"
222+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
223+ xml:space="preserve"
224+ inkscape:export-xdpi="61.120499"
225+ inkscape:export-ydpi="61.120499"><tspan
226+ y="295.36218"
227+ x="201"
228+ sodipodi:role="line"
229+ id="tspan5080"
230+ style="font-size:15px;fill:#ff0000">Declare</tspan></text>
231+ <text
232+ xml:space="preserve"
233+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
234+ x="117"
235+ y="344.36218"
236+ id="text5082"
237+ sodipodi:linespacing="125%"
238+ inkscape:export-xdpi="61.120499"
239+ inkscape:export-ydpi="61.120499"><tspan
240+ style="font-size:15px;fill:#0000ff"
241+ sodipodi:role="line"
242+ id="tspan5084"
243+ x="117"
244+ y="344.36218">name:TTName</tspan><tspan
245+ style="font-size:15px;fill:#0000ff"
246+ id="tspan5086"
247+ sodipodi:role="line"
248+ x="117"
249+ y="363.11218">arguments:List FunArg</tspan><tspan
250+ style="font-size:15px;fill:#0000ff"
251+ id="tspan5088"
252+ sodipodi:role="line"
253+ x="117"
254+ y="381.86218">returnType:Raw</tspan></text>
255+ <text
256+ xml:space="preserve"
257+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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;"
258+ x="111"
259+ y="313.36218"
260+ id="text5095"
261+ sodipodi:linespacing="125%"
262+ inkscape:export-xdpi="61.120499"
263+ inkscape:export-ydpi="61.120499"><tspan
264+ style="font-size:15px;fill:#0000ff;"
265+ id="tspan5097"
266+ sodipodi:role="line"
267+ x="111"
268+ y="313.36218">TyDecl</tspan></text>
269+ <rect
270+ 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"
271+ id="rect5099"
272+ width="125"
273+ height="88"
274+ x="170"
275+ y="415.36218"
276+ inkscape:export-xdpi="61.120499"
277+ inkscape:export-ydpi="61.120499" />
278+ <path
279+ inkscape:connector-curvature="0"
280+ id="path5101"
281+ d="m 247,364.3622 0,48"
282+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
283+ inkscape:export-xdpi="61.120499"
284+ inkscape:export-ydpi="61.120499" />
285+ <text
286+ xml:space="preserve"
287+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
288+ x="260"
289+ y="408.36218"
290+ id="text5103"
291+ sodipodi:linespacing="125%"
292+ inkscape:export-xdpi="61.120499"
293+ inkscape:export-ydpi="61.120499"><tspan
294+ style="font-size:15px;fill:#ff0000"
295+ id="tspan5105"
296+ sodipodi:role="line"
297+ x="260"
298+ y="408.36218">MkFunArg</tspan></text>
299+ <text
300+ sodipodi:linespacing="125%"
301+ id="text5107"
302+ y="437.36218"
303+ x="174"
304+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
305+ xml:space="preserve"
306+ inkscape:export-xdpi="61.120499"
307+ inkscape:export-ydpi="61.120499"><tspan
308+ y="437.36218"
309+ x="174"
310+ id="tspan5109"
311+ sodipodi:role="line"
312+ style="font-size:15px;fill:#0000ff">name:TTName</tspan><tspan
313+ y="456.11218"
314+ x="174"
315+ sodipodi:role="line"
316+ id="tspan5113"
317+ style="font-size:15px;fill:#0000ff">type:Raw</tspan><tspan
318+ y="474.86218"
319+ x="174"
320+ sodipodi:role="line"
321+ style="font-size:15px;fill:#0000ff"
322+ id="tspan5121">plicity:Plicity</tspan><tspan
323+ y="493.61218"
324+ x="174"
325+ sodipodi:role="line"
326+ style="font-size:15px;fill:#0000ff"
327+ id="tspan5123">erasure:Erasure</tspan></text>
328+ <text
329+ sodipodi:linespacing="125%"
330+ id="text5115"
331+ y="409.36218"
332+ x="170"
333+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
334+ xml:space="preserve"
335+ inkscape:export-xdpi="61.120499"
336+ inkscape:export-ydpi="61.120499"><tspan
337+ y="409.36218"
338+ x="170"
339+ sodipodi:role="line"
340+ id="tspan5117"
341+ style="font-size:15px;fill:#0000ff">FunArg</tspan></text>
342+ <text
343+ sodipodi:linespacing="125%"
344+ id="text5125"
345+ y="526.36218"
346+ x="105"
347+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
348+ xml:space="preserve"
349+ inkscape:export-xdpi="61.120499"
350+ inkscape:export-ydpi="61.120499"><tspan
351+ y="526.36218"
352+ x="105"
353+ sodipodi:role="line"
354+ id="tspan5127"
355+ style="font-size:15px;fill:#ff0000">Explicit</tspan><tspan
356+ y="545.11218"
357+ x="105"
358+ sodipodi:role="line"
359+ style="font-size:15px;fill:#ff0000"
360+ id="tspan5129">Implicit</tspan><tspan
361+ y="563.86218"
362+ x="105"
363+ sodipodi:role="line"
364+ style="font-size:15px;fill:#ff0000"
365+ id="tspan5131">Constraint</tspan></text>
366+ <path
367+ inkscape:connector-curvature="0"
368+ id="path5161"
369+ d="m 169,473.3622 c -30.23945,2.9603 -39.98191,17.10078 -41,36"
370+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5163)"
371+ sodipodi:nodetypes="cc"
372+ inkscape:export-xdpi="61.120499"
373+ inkscape:export-ydpi="61.120499" />
374+ <path
375+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker6325)"
376+ d="m 245,499.3622 0,28"
377+ id="path6319"
378+ inkscape:connector-curvature="0"
379+ sodipodi:nodetypes="cc"
380+ inkscape:export-xdpi="61.120499"
381+ inkscape:export-ydpi="61.120499" />
382+ <text
383+ sodipodi:linespacing="125%"
384+ id="text6321"
385+ y="544.36218"
386+ x="221"
387+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
388+ xml:space="preserve"
389+ inkscape:export-xdpi="61.120499"
390+ inkscape:export-ydpi="61.120499"><tspan
391+ y="544.36218"
392+ x="221"
393+ sodipodi:role="line"
394+ id="tspan6323"
395+ style="font-size:15px;fill:#ff0000">Erased</tspan><tspan
396+ y="563.11218"
397+ x="221"
398+ sodipodi:role="line"
399+ style="font-size:15px;fill:#ff0000"
400+ id="tspan6773">NotErased</tspan></text>
401+ <rect
402+ 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"
403+ id="rect6775"
404+ width="247"
405+ height="49"
406+ x="347"
407+ y="322.36218"
408+ inkscape:export-xdpi="61.120499"
409+ inkscape:export-ydpi="61.120499" />
410+ <path
411+ inkscape:connector-curvature="0"
412+ id="path6777"
413+ d="m 458,271.3622 0,48"
414+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5133)"
415+ inkscape:export-xdpi="61.120499"
416+ inkscape:export-ydpi="61.120499" />
417+ <text
418+ xml:space="preserve"
419+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
420+ x="469"
421+ y="295.36218"
422+ id="text6779"
423+ sodipodi:linespacing="125%"
424+ inkscape:export-xdpi="61.120499"
425+ inkscape:export-ydpi="61.120499"><tspan
426+ style="font-size:15px;fill:#ff0000"
427+ id="tspan6781"
428+ sodipodi:role="line"
429+ x="469"
430+ y="295.36218">DefineFun</tspan></text>
431+ <text
432+ sodipodi:linespacing="125%"
433+ id="text6783"
434+ y="344.36218"
435+ x="351"
436+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
437+ xml:space="preserve"
438+ inkscape:export-xdpi="61.120499"
439+ inkscape:export-ydpi="61.120499"><tspan
440+ y="344.36218"
441+ x="351"
442+ sodipodi:role="line"
443+ id="tspan6789"
444+ style="font-size:15px;fill:#0000ff">name:TTName</tspan><tspan
445+ y="363.11218"
446+ x="351"
447+ sodipodi:role="line"
448+ style="font-size:15px;fill:#0000ff"
449+ id="tspan7130">clauses : List (FunClause a)</tspan></text>
450+ <text
451+ sodipodi:linespacing="125%"
452+ id="text6791"
453+ y="313.36218"
454+ x="379"
455+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
456+ xml:space="preserve"
457+ inkscape:export-xdpi="61.120499"
458+ inkscape:export-ydpi="61.120499"><tspan
459+ y="313.36218"
460+ x="379"
461+ sodipodi:role="line"
462+ id="tspan6793"
463+ style="font-size:15px;fill:#0000ff">FunDefn</tspan></text>
464+ <rect
465+ 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"
466+ id="rect6799"
467+ width="86"
468+ height="64"
469+ x="372"
470+ y="462.36218"
471+ inkscape:export-xdpi="61.120499"
472+ inkscape:export-ydpi="61.120499" />
473+ <path
474+ inkscape:connector-curvature="0"
475+ id="path6801"
476+ d="m 552,370.3622 0,86"
477+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker6819)"
478+ inkscape:export-xdpi="61.120499"
479+ inkscape:export-ydpi="61.120499"
480+ sodipodi:nodetypes="cc" />
481+ <text
482+ xml:space="preserve"
483+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
484+ x="352"
485+ y="418.36218"
486+ id="text6803"
487+ sodipodi:linespacing="125%"
488+ inkscape:export-xdpi="61.120499"
489+ inkscape:export-ydpi="61.120499"><tspan
490+ style="font-size:15px;fill:#ff0000"
491+ id="tspan6805"
492+ sodipodi:role="line"
493+ x="352"
494+ y="418.36218">MkFunClause</tspan></text>
495+ <text
496+ sodipodi:linespacing="125%"
497+ id="text6807"
498+ y="484.36218"
499+ x="376"
500+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
501+ xml:space="preserve"
502+ inkscape:export-xdpi="61.120499"
503+ inkscape:export-ydpi="61.120499"><tspan
504+ y="484.36218"
505+ x="376"
506+ sodipodi:role="line"
507+ id="tspan6813"
508+ style="font-size:15px;fill:#0000ff">lhs:a</tspan><tspan
509+ y="503.11218"
510+ x="376"
511+ sodipodi:role="line"
512+ style="font-size:15px;fill:#0000ff"
513+ id="tspan4330">rhs:a</tspan></text>
514+ <text
515+ sodipodi:linespacing="125%"
516+ id="text6815"
517+ y="453.36218"
518+ x="370"
519+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
520+ xml:space="preserve"
521+ inkscape:export-xdpi="61.120499"
522+ inkscape:export-ydpi="61.120499"><tspan
523+ y="453.36218"
524+ x="370"
525+ sodipodi:role="line"
526+ id="tspan6817"
527+ style="font-size:15px;fill:#0000ff">FunClause</tspan></text>
528+ <text
529+ inkscape:export-ydpi="61.120499"
530+ inkscape:export-xdpi="61.120499"
531+ sodipodi:linespacing="125%"
532+ id="text4321"
533+ y="395.36218"
534+ x="407"
535+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
536+ xml:space="preserve"><tspan
537+ y="395.36218"
538+ x="407"
539+ sodipodi:role="line"
540+ id="tspan4323"
541+ style="font-size:15px;fill:#ff0000">MkImpossibleClause</tspan></text>
542+ <rect
543+ inkscape:export-ydpi="61.120499"
544+ inkscape:export-xdpi="61.120499"
545+ y="461.36218"
546+ x="473"
547+ height="64"
548+ width="86"
549+ id="rect4332"
550+ 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" />
551+ <text
552+ inkscape:export-ydpi="61.120499"
553+ inkscape:export-xdpi="61.120499"
554+ xml:space="preserve"
555+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
556+ x="477"
557+ y="483.36218"
558+ id="text4334"
559+ sodipodi:linespacing="125%"><tspan
560+ id="tspan4338"
561+ style="font-size:15px;fill:#0000ff"
562+ sodipodi:role="line"
563+ x="477"
564+ y="483.36218">lhs:a</tspan></text>
565+ <text
566+ inkscape:export-ydpi="61.120499"
567+ inkscape:export-xdpi="61.120499"
568+ xml:space="preserve"
569+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
570+ x="471"
571+ y="452.36218"
572+ id="text4340"
573+ sodipodi:linespacing="125%"><tspan
574+ style="font-size:15px;fill:#0000ff"
575+ id="tspan4342"
576+ sodipodi:role="line"
577+ x="471"
578+ y="452.36218">FunClause</tspan></text>
579+ <path
580+ inkscape:export-ydpi="61.120499"
581+ inkscape:export-xdpi="61.120499"
582+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4348)"
583+ d="m 450,371.3622 0,84"
584+ id="path4346"
585+ inkscape:connector-curvature="0"
586+ sodipodi:nodetypes="cc" />
587+ </g>
588+</svg>
docs/proofs/generatingData.rst+22−2
@@ -61,6 +61,21 @@ Here is a simple example constructing a boolean type:
61Generating Functions
61Generating Functions
62--------------------
62--------------------
63
63
64+There are two main 'tactics' associated with generating functions:
65+
66+- declareType
67+- defineFunction
68+
69+Which declare and define the function as the names suggest.
70+
71+.. list-table::
72+
73+ * - These 'tactics' and the data structures associated with them are listed in the tables later on this page, for now, here is a summary:
74+ - .. image:: ../image/generateFunction.png
75+ :width: 332px
76+ :height: 246px
77+ :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
78+
64We can now add some function definitions to the above datatype:
79We can now add some function definitions to the above datatype:
65
80
66.. code-block:: idris
81.. code-block:: idris
@@ -144,10 +159,12 @@ Which can be used like this:
144 λΠ> :t MkN
159 λΠ> :t MkN
145 MkN : N x
160 MkN : N x
146
161
162+Table of 'tactics' for Generating Data and Functions
163+----------------------------------------------------
147
164
148These are the functions that we can use to create data and functions in the Elab monad:
165These are the functions that we can use to create data and functions in the Elab monad:
149
166
150−.. list-table:: Generating Data and Functions
167+.. list-table::
151 :widths: 10 30
168 :widths: 10 30
152 :stub-columns: 1
169 :stub-columns: 1
153
170
@@ -199,9 +216,12 @@ These are the functions that we can use to create data and functions in the Elab
199
216
200 isTCName : (name : TTName) -> Elab Bool
217 isTCName : (name : TTName) -> Elab Bool
201
218
219+Table of Datatypes Associated with Generating Data and Functions
220+----------------------------------------------------------------
221+
202The above functions use the following data/records:
222The above functions use the following data/records:
203
223
204−.. list-table:: Generating Data and Functions data/records
224+.. list-table::
205 :widths: 10 30
225 :widths: 10 30
206 :stub-columns: 1
226 :stub-columns: 1
207
227