on master help sign in
add example and diagram for fill
commitd73e3c531cf88be77ca74a3e1c4ffa83bf2b8bd0 authormartinbaker <git29f185@martinb.com> dateFri 5 Jul 2019, 07:58 (7 years ago) parenteda6a87
3 files changed+142
docs/image/fill.png docs/image/fill.svg+127 docs/proofs/primitive.rst+15
docs/image/fill.pngnew file

Binary file not shown.

docs/image/fill.svgnew file+127
@@ -0,0 +1,127 @@
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="fill.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="Arrow1Mend"
27+ style="overflow:visible;"
28+ inkscape:isstock="true">
29+ <path
30+ id="path4529"
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:#ff0000;stroke-width:1pt;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
33+ transform="scale(0.4) rotate(180) translate(10,0)" />
34+ </marker>
35+ </defs>
36+ <sodipodi:namedview
37+ id="base"
38+ pagecolor="#ffffff"
39+ bordercolor="#666666"
40+ borderopacity="1.0"
41+ inkscape:pageopacity="0.0"
42+ inkscape:pageshadow="2"
43+ inkscape:zoom="1"
44+ inkscape:cx="313.5"
45+ inkscape:cy="696.5"
46+ inkscape:document-units="mm"
47+ inkscape:current-layer="layer1"
48+ showgrid="false"
49+ inkscape:window-width="1920"
50+ inkscape:window-height="1015"
51+ inkscape:window-x="0"
52+ inkscape:window-y="0"
53+ inkscape:window-maximized="1" />
54+ <metadata
55+ id="metadata5">
56+ <rdf:RDF>
57+ <cc:Work
58+ rdf:about="">
59+ <dc:format>image/svg+xml</dc:format>
60+ <dc:type
61+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
62+ <dc:title></dc:title>
63+ </cc:Work>
64+ </rdf:RDF>
65+ </metadata>
66+ <g
67+ inkscape:label="Layer 1"
68+ inkscape:groupmode="layer"
69+ id="layer1">
70+ <rect
71+ style="fill:#ffff00;fill-opacity:1;stroke-width:0.26458332"
72+ id="rect22"
73+ width="31.75"
74+ height="5.5562501"
75+ x="80.697914"
76+ y="114.96667"
77+ inkscape:export-xdpi="61.120499"
78+ inkscape:export-ydpi="61.120499" />
79+ <text
80+ xml:space="preserve"
81+ 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"
82+ x="41.539581"
83+ y="104.64792"
84+ id="text12"
85+ inkscape:export-xdpi="61.120499"
86+ inkscape:export-ydpi="61.120499"><tspan
87+ sodipodi:role="line"
88+ id="tspan10"
89+ x="41.539581"
90+ y="104.64792"
91+ style="stroke-width:0.26458332;font-size:4.23333333px;-inkscape-font-specification:'sans-serif Bold';font-family:sans-serif;font-weight:bold;font-style:normal;font-stretch:normal;font-variant:normal">?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}</tspan></text>
92+ <text
93+ id="text16"
94+ y="119.2"
95+ x="41.539581"
96+ 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"
97+ xml:space="preserve"
98+ inkscape:export-xdpi="61.120499"
99+ inkscape:export-ydpi="61.120499"><tspan
100+ 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"
101+ y="119.2"
102+ x="41.539581"
103+ id="tspan14"
104+ sodipodi:role="line">?{hole_0} ≈ ?{hole_2} ≈ Prelude.Nat.Z . {hole_2} . {hole_0}</tspan></text>
105+ <text
106+ id="text20"
107+ y="110.99791"
108+ x="82.814583"
109+ 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"
110+ xml:space="preserve"
111+ inkscape:export-xdpi="61.120499"
112+ inkscape:export-ydpi="61.120499"><tspan
113+ 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"
114+ y="110.99791"
115+ x="82.814583"
116+ id="tspan18"
117+ sodipodi:role="line">fill `(Z)</tspan></text>
118+ <path
119+ 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)"
120+ d="m 80.668481,106.30075 -0.0032,7.57492"
121+ id="path4518"
122+ inkscape:connector-curvature="0"
123+ sodipodi:nodetypes="cc"
124+ inkscape:export-xdpi="61.120499"
125+ inkscape:export-ydpi="61.120499" />
126+ </g>
127+</svg>
docs/proofs/primitive.rst+15
@@ -30,6 +30,11 @@ Primitive Operators
3030 * - fill
3131 - Place a term into a hole, unifying its type. Fails if the focus is not a hole.
3232
33+ - .. image:: ../image/fill.png
34+ :width: 259px
35+ :height: 46px
36+ :alt: diagram illustrating fill tactic
37+
3338 Signature:
3439
3540 fill : (e : Raw) -> Elab ()
@@ -46,6 +51,16 @@ Primitive Operators
4651
4752 This unification can result in the solution of further holes or the establishment of additional unsolved unification constraints.
4853
54+ Example:
55+
56+ .. code-block:: idris
57+
58+ %language ElabReflection
59+
60+ testFn : Nat
61+ testFn = %runElab (do fill `(Z)
62+ solve)
63+
4964 * - apply
5065 - Attempt to apply an operator to fill the current hole, potentially solving arguments by unification.
5166