d0a4575 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

further improvements from comments

commitd0a45759127edf15f188d5e3756b580ecdd68096 authorMartin Baker <git87465@martinb.com> dateWed 15 May 2019, 17:43 (7 years ago) parent9472245

15 files changed+3039

compare with master

unifiedsplit

docs/image/binders.svg+326 docs/image/compareToProofAssist.png docs/image/compareToProofAssist.svg+251 docs/image/elab.svg+139 docs/image/elabLogicEx1_1.svg+97 docs/image/elabLogicEx1_2.svg+115 docs/image/elabLogicEx1_3.svg+115 docs/image/elabLogicEx1_4.svg+80 docs/image/elabProofState.svg+356 docs/image/elabProofStateEx1_1.svg+311 docs/image/elabProofStateEx1_2.svg+271 docs/image/elabProofStateEx1_3.svg+274 docs/image/idrisTopLevel.png docs/image/idrisTopLevel.svg+524 docs/image/tree.svg+180

docs/image/binders.svgnew file+326

@@ -0,0 +1,326 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="binders.svg">

19+ <defs

20+ id="defs4" />

21+ <sodipodi:namedview

22+ id="base"

23+ pagecolor="#ffffff"

24+ bordercolor="#666666"

25+ borderopacity="1.0"

26+ inkscape:pageopacity="0.0"

27+ inkscape:pageshadow="2"

28+ inkscape:zoom="1"

29+ inkscape:cx="255.00889"

30+ inkscape:cy="520"

31+ inkscape:document-units="px"

32+ inkscape:current-layer="layer1"

33+ showgrid="false"

34+ inkscape:window-width="1163"

35+ inkscape:window-height="1011"

36+ inkscape:window-x="-4"

37+ inkscape:window-y="0"

38+ inkscape:window-maximized="0" />

39+ <metadata

40+ id="metadata7">

41+ <rdf:RDF>

42+ <cc:Work

43+ rdf:about="">

44+ <dc:format>image/svg+xml</dc:format>

45+ <dc:type

46+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

47+ <dc:title></dc:title>

48+ </cc:Work>

49+ </rdf:RDF>

50+ </metadata>

51+ <g

52+ inkscape:label="Layer 1"

53+ inkscape:groupmode="layer"

54+ id="layer1">

55+ <text

56+ xml:space="preserve"

57+ style="font-style:normal;font-weight:normal;font-size:40px;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;"

58+ x="157"

59+ y="177.3622"

60+ id="text4136"

61+ sodipodi:linespacing="125%"

62+ inkscape:export-xdpi="61.120499"

63+ inkscape:export-ydpi="61.120499"><tspan

64+ sodipodi:role="line"

65+ id="tspan4138"

66+ x="157"

67+ y="177.3622"

68+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;">Code</tspan></text>

69+ <text

70+ sodipodi:linespacing="125%"

71+ id="text4140"

72+ y="177.3622"

73+ x="287"

74+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

75+ xml:space="preserve"

76+ inkscape:export-xdpi="61.120499"

77+ inkscape:export-ydpi="61.120499"><tspan

78+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;"

79+ y="177.3622"

80+ x="287"

81+ id="tspan4142"

82+ sodipodi:role="line">Logic</tspan></text>

83+ <path

84+ 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"

85+ d="m 229,161.3622 1,298"

86+ id="path4144"

87+ inkscape:connector-curvature="0"

88+ sodipodi:nodetypes="cc"

89+ inkscape:export-xdpi="61.120499"

90+ inkscape:export-ydpi="61.120499" />

91+ <path

92+ inkscape:connector-curvature="0"

93+ id="path4146"

94+ d="m 473.5,184.8622 -364,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+ sodipodi:nodetypes="cc"

97+ inkscape:export-xdpi="61.120499"

98+ inkscape:export-ydpi="61.120499" />

99+ <path

100+ 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"

101+ d="m 473.5,270.8622 -364,1"

102+ id="path4148"

103+ inkscape:connector-curvature="0"

104+ sodipodi:nodetypes="cc"

105+ inkscape:export-xdpi="61.120499"

106+ inkscape:export-ydpi="61.120499" />

107+ <path

108+ inkscape:connector-curvature="0"

109+ id="path4150"

110+ d="m 475.5,362.8622 -366,1"

111+ 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"

112+ sodipodi:nodetypes="cc"

113+ inkscape:export-xdpi="61.120499"

114+ inkscape:export-ydpi="61.120499" />

115+ <path

116+ 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"

117+ d="m 475.5,458.8622 -366,1"

118+ id="path4152"

119+ inkscape:connector-curvature="0"

120+ sodipodi:nodetypes="cc"

121+ inkscape:export-xdpi="61.120499"

122+ inkscape:export-ydpi="61.120499" />

123+ <text

124+ sodipodi:linespacing="125%"

125+ id="text4154"

126+ y="235.3622"

127+ x="19"

128+ style="font-style:normal;font-weight:normal;font-size:40px;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"

129+ xml:space="preserve"

130+ inkscape:export-xdpi="61.120499"

131+ inkscape:export-ydpi="61.120499"><tspan

132+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

133+ y="235.3622"

134+ x="19"

135+ id="tspan4156"

136+ sodipodi:role="line">Abstraction</tspan></text>

137+ <text

138+ xml:space="preserve"

139+ style="font-style:normal;font-weight:normal;font-size:40px;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"

140+ x="19"

141+ y="399.36218"

142+ id="text4158"

143+ sodipodi:linespacing="125%"

144+ inkscape:export-xdpi="61.120499"

145+ inkscape:export-ydpi="61.120499"><tspan

146+ sodipodi:role="line"

147+ id="tspan4160"

148+ x="19"

149+ y="399.36218"

150+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">let</tspan><tspan

151+ sodipodi:role="line"

152+ x="19"

153+ y="424.36218"

154+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

155+ id="tspan4184">binding</tspan></text>

156+ <text

157+ sodipodi:linespacing="125%"

158+ id="text4162"

159+ y="307.36218"

160+ x="19"

161+ style="font-style:normal;font-weight:normal;font-size:40px;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"

162+ xml:space="preserve"

163+ inkscape:export-xdpi="61.120499"

164+ inkscape:export-ydpi="61.120499"><tspan

165+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

166+ y="307.36218"

167+ x="19"

168+ id="tspan4164"

169+ sodipodi:role="line">function</tspan><tspan

170+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

171+ y="332.36218"

172+ x="19"

173+ sodipodi:role="line"

174+ id="tspan4166">space</tspan></text>

175+ <text

176+ xml:space="preserve"

177+ style="font-style:normal;font-weight:normal;font-size:40px;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;"

178+ x="167"

179+ y="235.3622"

180+ id="text4168"

181+ sodipodi:linespacing="125%"

182+ inkscape:export-xdpi="61.120499"

183+ inkscape:export-ydpi="61.120499"><tspan

184+ sodipodi:role="line"

185+ id="tspan4170"

186+ x="167"

187+ y="235.3622"

188+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;">λ x:t</tspan></text>

189+ <text

190+ sodipodi:linespacing="125%"

191+ id="text4172"

192+ y="222.3622"

193+ x="259"

194+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

195+ xml:space="preserve"

196+ inkscape:export-xdpi="61.120499"

197+ inkscape:export-ydpi="61.120499"><tspan

198+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;"

199+ y="222.3622"

200+ x="259"

201+ id="tspan4174"

202+ sodipodi:role="line">Γ ⊢ S : Type</tspan></text>

203+ <text

204+ sodipodi:linespacing="125%"

205+ id="text4180"

206+ y="417.36218"

207+ x="124"

208+ style="font-style:normal;font-weight:normal;font-size:40px;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;"

209+ xml:space="preserve"

210+ inkscape:export-xdpi="61.120499"

211+ inkscape:export-ydpi="61.120499"><tspan

212+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;"

213+ y="417.36218"

214+ x="124"

215+ id="tspan4182"

216+ sodipodi:role="line">let x ↦ t : t</tspan></text>

217+ <path

218+ inkscape:connector-curvature="0"

219+ id="path4186"

220+ d="m 383.5,227.8622 -136,1"

221+ 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"

222+ sodipodi:nodetypes="cc"

223+ inkscape:export-xdpi="61.120499"

224+ inkscape:export-ydpi="61.120499" />

225+ <text

226+ xml:space="preserve"

227+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

228+ x="246"

229+ y="248.3622"

230+ id="text4188"

231+ sodipodi:linespacing="125%"

232+ inkscape:export-xdpi="61.120499"

233+ inkscape:export-ydpi="61.120499"><tspan

234+ sodipodi:role="line"

235+ id="tspan4190"

236+ x="246"

237+ y="248.3622"

238+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;">Γ ; λ x:S ⊢ valid</tspan></text>

239+ <text

240+ xml:space="preserve"

241+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

242+ x="257"

243+ y="308.36218"

244+ id="text4192"

245+ sodipodi:linespacing="125%"

246+ inkscape:export-xdpi="61.120499"

247+ inkscape:export-ydpi="61.120499"><tspan

248+ sodipodi:role="line"

249+ id="tspan4194"

250+ x="257"

251+ y="308.36218"

252+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;">Γ ⊢ S : Type</tspan></text>

253+ <path

254+ sodipodi:nodetypes="cc"

255+ 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"

256+ d="m 381.5,313.8622 -136,1"

257+ id="path4196"

258+ inkscape:connector-curvature="0"

259+ inkscape:export-xdpi="61.120499"

260+ inkscape:export-ydpi="61.120499" />

261+ <text

262+ sodipodi:linespacing="125%"

263+ id="text4198"

264+ y="334.36218"

265+ x="244"

266+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

267+ xml:space="preserve"

268+ inkscape:export-xdpi="61.120499"

269+ inkscape:export-ydpi="61.120499"><tspan

270+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;"

271+ y="334.36218"

272+ x="244"

273+ id="tspan4200"

274+ sodipodi:role="line">Γ ; ∀ x:S ⊢ valid</tspan></text>

275+ <text

276+ xml:space="preserve"

277+ style="font-style:normal;font-weight:normal;font-size:40px;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;"

278+ x="167"

279+ y="323.36218"

280+ id="text4202"

281+ sodipodi:linespacing="125%"

282+ inkscape:export-xdpi="61.120499"

283+ inkscape:export-ydpi="61.120499"><tspan

284+ sodipodi:role="line"

285+ id="tspan4204"

286+ x="167"

287+ y="323.36218"

288+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;">∀ x:t</tspan></text>

289+ <text

290+ sodipodi:linespacing="125%"

291+ id="text4206"

292+ y="402.36218"

293+ x="255"

294+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

295+ xml:space="preserve"

296+ inkscape:export-xdpi="61.120499"

297+ inkscape:export-ydpi="61.120499"><tspan

298+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;"

299+ y="402.36218"

300+ x="255"

301+ id="tspan4208"

302+ sodipodi:role="line">Γ ⊢ S : Type Γ ⊢ s:S </tspan></text>

303+ <path

304+ inkscape:connector-curvature="0"

305+ id="path4210"

306+ d="m 453.5,407.8622 -210,1"

307+ 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"

308+ sodipodi:nodetypes="cc"

309+ inkscape:export-xdpi="61.120499"

310+ inkscape:export-ydpi="61.120499" />

311+ <text

312+ xml:space="preserve"

313+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;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;"

314+ x="242"

315+ y="428.36218"

316+ id="text4212"

317+ sodipodi:linespacing="125%"

318+ inkscape:export-xdpi="61.120499"

319+ inkscape:export-ydpi="61.120499"><tspan

320+ sodipodi:role="line"

321+ id="tspan4214"

322+ x="242"

323+ y="428.36218"

324+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;">Γ ; let x ↦ s : S ⊢ valid</tspan></text>

325+ </g>

326+</svg>

docs/image/compareToProofAssist.png

Binary file not shown.

docs/image/compareToProofAssist.svgnew file+251

@@ -0,0 +1,251 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="compareToProofAssist.svg">

19+ <defs

20+ id="defs4">

21+ <marker

22+ inkscape:stockid="Arrow1Mend"

23+ orient="auto"

24+ refY="0.0"

25+ refX="0.0"

26+ id="marker5018"

27+ style="overflow:visible;"

28+ inkscape:isstock="true">

29+ <path

30+ id="path5020"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="marker4436"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="path4438" />

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="path4167"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="377.89372"

75+ inkscape:cy="520"

76+ inkscape:document-units="px"

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="metadata7">

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></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+ <text

101+ xml:space="preserve"

102+ style="font-style:normal;font-weight:normal;font-size:40px;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"

103+ x="162"

104+ y="326.36221"

105+ id="text4136"

106+ sodipodi:linespacing="125%"

107+ inkscape:export-xdpi="61.120499"

108+ inkscape:export-ydpi="61.120499"><tspan

109+ sodipodi:role="line"

110+ id="tspan4138"

111+ x="162"

112+ y="326.36221"

113+ style="font-size:15px;-inkscape-font-specification:'sans-serif Bold';font-family:sans-serif;font-weight:bold;font-style:normal;font-stretch:normal;font-variant:normal">Human</tspan></text>

114+ <text

115+ sodipodi:linespacing="125%"

116+ id="text4140"

117+ y="368.36221"

118+ x="162"

119+ style="font-style:normal;font-weight:normal;font-size:40px;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"

120+ xml:space="preserve"

121+ inkscape:export-xdpi="61.120499"

122+ inkscape:export-ydpi="61.120499"><tspan

123+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

124+ y="368.36221"

125+ x="162"

126+ id="tspan4142"

127+ sodipodi:role="line">Tactics</tspan></text>

128+ <text

129+ xml:space="preserve"

130+ style="font-style:normal;font-weight:normal;font-size:40px;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"

131+ x="161"

132+ y="415.36221"

133+ id="text4144"

134+ sodipodi:linespacing="125%"

135+ inkscape:export-xdpi="61.120499"

136+ inkscape:export-ydpi="61.120499"><tspan

137+ sodipodi:role="line"

138+ id="tspan4146"

139+ x="161"

140+ y="415.36221"

141+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">fill holes</tspan></text>

142+ <text

143+ sodipodi:linespacing="125%"

144+ id="text4148"

145+ y="282.36221"

146+ x="130"

147+ style="font-style:normal;font-weight:normal;font-size:40px;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;"

148+ xml:space="preserve"

149+ inkscape:export-xdpi="61.120499"

150+ inkscape:export-ydpi="61.120499"><tspan

151+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;"

152+ y="282.36221"

153+ x="130"

154+ id="tspan4150"

155+ sodipodi:role="line">Proof assistant</tspan></text>

156+ <path

157+ 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;marker-end:url(#Arrow1Mend)"

158+ d="m 188,329.3622 0,22"

159+ id="path4152"

160+ inkscape:connector-curvature="0"

161+ inkscape:export-xdpi="61.120499"

162+ inkscape:export-ydpi="61.120499" />

163+ <path

164+ inkscape:connector-curvature="0"

165+ id="path4434"

166+ d="m 187,373.3622 0,22"

167+ 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;marker-end:url(#marker4436)"

168+ inkscape:export-xdpi="61.120499"

169+ inkscape:export-ydpi="61.120499" />

170+ <text

171+ sodipodi:linespacing="125%"

172+ id="text4998"

173+ y="307.36221"

174+ x="306"

175+ style="font-style:normal;font-weight:normal;font-size:40px;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"

176+ xml:space="preserve"

177+ inkscape:export-xdpi="61.120499"

178+ inkscape:export-ydpi="61.120499"><tspan

179+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

180+ y="307.36221"

181+ x="306"

182+ id="tspan5000"

183+ sodipodi:role="line">High level program</tspan><tspan

184+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

185+ y="326.11221"

186+ x="306"

187+ sodipodi:role="line"

188+ id="tspan5058">(unification algorithm)</tspan></text>

189+ <text

190+ xml:space="preserve"

191+ style="font-style:normal;font-weight:normal;font-size:40px;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"

192+ x="316"

193+ y="369.36221"

194+ id="text5002"

195+ sodipodi:linespacing="125%"

196+ inkscape:export-xdpi="61.120499"

197+ inkscape:export-ydpi="61.120499"><tspan

198+ sodipodi:role="line"

199+ id="tspan5004"

200+ x="316"

201+ y="369.36221"

202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Tactics</tspan></text>

203+ <text

204+ sodipodi:linespacing="125%"

205+ id="text5006"

206+ y="416.36221"

207+ x="315"

208+ style="font-style:normal;font-weight:normal;font-size:40px;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"

209+ xml:space="preserve"

210+ inkscape:export-xdpi="61.120499"

211+ inkscape:export-ydpi="61.120499"><tspan

212+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

213+ y="416.36221"

214+ x="315"

215+ id="tspan5008"

216+ sodipodi:role="line">fill holes</tspan><tspan

217+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

218+ y="435.11221"

219+ x="315"

220+ sodipodi:role="line"

221+ id="tspan5060">(implicit variables, etc)</tspan></text>

222+ <text

223+ xml:space="preserve"

224+ style="font-style:normal;font-weight:normal;font-size:40px;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"

225+ x="294"

226+ y="282.36221"

227+ id="text5010"

228+ sodipodi:linespacing="125%"

229+ inkscape:export-xdpi="61.120499"

230+ inkscape:export-ydpi="61.120499"><tspan

231+ sodipodi:role="line"

232+ id="tspan5012"

233+ x="294"

234+ y="282.36221"

235+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000">Idris Elaborator</tspan></text>

236+ <path

237+ inkscape:connector-curvature="0"

238+ id="path5014"

239+ d="m 342,330.3622 0,22"

240+ 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;marker-end:url(#Arrow1Mend)"

241+ inkscape:export-xdpi="61.120499"

242+ inkscape:export-ydpi="61.120499" />

243+ <path

244+ 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;marker-end:url(#marker5018)"

245+ d="m 341,374.3622 0,22"

246+ id="path5016"

247+ inkscape:connector-curvature="0"

248+ inkscape:export-xdpi="61.120499"

249+ inkscape:export-ydpi="61.120499" />

250+ </g>

251+</svg>

docs/image/elab.svgnew file+139

@@ -0,0 +1,139 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elab.svg">

19+ <defs

20+ id="defs4">

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="path4155"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="381.03373"

45+ inkscape:cy="520"

46+ inkscape:document-units="px"

47+ inkscape:current-layer="layer1"

48+ showgrid="false"

49+ inkscape:window-width="1072"

50+ inkscape:window-height="1011"

51+ inkscape:window-x="-4"

52+ inkscape:window-y="0"

53+ inkscape:window-maximized="0" />

54+ <metadata

55+ id="metadata7">

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="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

72+ id="rect4136"

73+ width="206"

74+ height="77"

75+ x="236"

76+ y="254.3622"

77+ inkscape:export-xdpi="61.120499"

78+ inkscape:export-ydpi="61.120499" />

79+ <rect

80+ y="388.36218"

81+ x="236"

82+ height="77"

83+ width="206"

84+ id="rect4138"

85+ 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"

86+ inkscape:export-xdpi="61.120499"

87+ inkscape:export-ydpi="61.120499" />

88+ <path

89+ 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;marker-end:url(#Arrow1Mend)"

90+ d="m 328,331.3622 19,55"

91+ id="path4140"

92+ inkscape:connector-curvature="0"

93+ sodipodi:nodetypes="cc"

94+ inkscape:export-xdpi="61.120499"

95+ inkscape:export-ydpi="61.120499" />

96+ <text

97+ xml:space="preserve"

98+ 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"

99+ x="242"

100+ y="271.36221"

101+ id="text5334"

102+ sodipodi:linespacing="125%"

103+ inkscape:export-xdpi="61.120499"

104+ inkscape:export-ydpi="61.120499"><tspan

105+ sodipodi:role="line"

106+ id="tspan5336"

107+ x="242"

108+ y="271.36221"

109+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Definition Elaborator</tspan></text>

110+ <text

111+ sodipodi:linespacing="125%"

112+ id="text5338"

113+ y="308.36221"

114+ x="253"

115+ 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"

116+ xml:space="preserve"

117+ inkscape:export-xdpi="61.120499"

118+ inkscape:export-ydpi="61.120499"><tspan

119+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

120+ y="308.36221"

121+ x="253"

122+ id="tspan5340"

123+ sodipodi:role="line">definition context</tspan></text>

124+ <text

125+ xml:space="preserve"

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:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"

127+ x="243"

128+ y="409.36221"

129+ id="text5342"

130+ sodipodi:linespacing="125%"

131+ inkscape:export-xdpi="61.120499"

132+ inkscape:export-ydpi="61.120499"><tspan

133+ sodipodi:role="line"

134+ id="tspan5344"

135+ x="243"

136+ y="409.36221"

137+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">Term Elaborator</tspan></text>

138+ </g>

139+</svg>

docs/image/elabLogicEx1_1.svgnew file+97

@@ -0,0 +1,97 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabLogicEx1_1.svg"

19+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"

20+ inkscape:export-xdpi="61.120499"

21+ inkscape:export-ydpi="61.120499">

22+ <defs

23+ id="defs4" />

24+ <sodipodi:namedview

25+ id="base"

26+ pagecolor="#ffffff"

27+ bordercolor="#666666"

28+ borderopacity="1.0"

29+ inkscape:pageopacity="0.0"

30+ inkscape:pageshadow="2"

31+ inkscape:zoom="1"

32+ inkscape:cx="425.25613"

33+ inkscape:cy="593.17666"

34+ inkscape:document-units="px"

35+ inkscape:current-layer="layer1"

36+ showgrid="false"

37+ inkscape:window-width="1131"

38+ inkscape:window-height="1011"

39+ inkscape:window-x="-4"

40+ inkscape:window-y="0"

41+ inkscape:window-maximized="0" />

42+ <metadata

43+ id="metadata7">

44+ <rdf:RDF>

45+ <cc:Work

46+ rdf:about="">

47+ <dc:format>image/svg+xml</dc:format>

48+ <dc:type

49+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

50+ <dc:title></dc:title>

51+ </cc:Work>

52+ </rdf:RDF>

53+ </metadata>

54+ <g

55+ inkscape:label="Layer 1"

56+ inkscape:groupmode="layer"

57+ id="layer1">

58+ <text

59+ sodipodi:linespacing="125%"

60+ id="text4800"

61+ y="473.36218"

62+ 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"

64+ xml:space="preserve"

65+ inkscape:export-xdpi="61.120499"

66+ 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'"

68+ y="473.36218"

69+ x="205"

70+ sodipodi:role="line"

71+ id="tspan4812">hole_2 : pi_arg : Nat -> Nat</tspan></text>

72+ <text

73+ inkscape:export-ydpi="61.120499"

74+ inkscape:export-xdpi="61.120499"

75+ 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"

77+ x="205"

78+ y="500.36218"

79+ id="text4178"

80+ sodipodi:linespacing="125%"><tspan

81+ id="tspan4180"

82+ sodipodi:role="line"

83+ x="205"

84+ y="500.36218"

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 -> Nat</tspan></text>

86+ <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"

88+ d="m 200,484.3622 185,-1"

89+ id="path4182"

90+ inkscape:connector-curvature="0" />

91+ <path

92+ inkscape:connector-curvature="0"

93+ id="path4184"

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" />

96+ </g>

97+</svg>

docs/image/elabLogicEx1_2.svgnew file+115

@@ -0,0 +1,115 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabLogicEx1_2.svg"

19+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"

20+ inkscape:export-xdpi="61.120499"

21+ inkscape:export-ydpi="61.120499">

22+ <defs

23+ id="defs4" />

24+ <sodipodi:namedview

25+ id="base"

26+ pagecolor="#ffffff"

27+ bordercolor="#666666"

28+ borderopacity="1.0"

29+ inkscape:pageopacity="0.0"

30+ inkscape:pageshadow="2"

31+ inkscape:zoom="1"

32+ inkscape:cx="425.25613"

33+ inkscape:cy="593.17666"

34+ inkscape:document-units="px"

35+ inkscape:current-layer="layer1"

36+ showgrid="false"

37+ inkscape:window-width="1920"

38+ inkscape:window-height="1015"

39+ inkscape:window-x="0"

40+ inkscape:window-y="0"

41+ inkscape:window-maximized="1" />

42+ <metadata

43+ id="metadata7">

44+ <rdf:RDF>

45+ <cc:Work

46+ rdf:about="">

47+ <dc:format>image/svg+xml</dc:format>

48+ <dc:type

49+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

50+ <dc:title />

51+ </cc:Work>

52+ </rdf:RDF>

53+ </metadata>

54+ <g

55+ inkscape:label="Layer 1"

56+ inkscape:groupmode="layer"

57+ id="layer1">

58+ <text

59+ sodipodi:linespacing="125%"

60+ id="text4800"

61+ y="473.36218"

62+ x="205"

64+ xml:space="preserve"

65+ inkscape:export-xdpi="61.120499"

66+ 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'"

68+ y="473.36218"

69+ x="205"

70+ sodipodi:role="line"

71+ id="tspan4812">hole_2 : Nat</tspan></text>

72+ <text

73+ inkscape:export-ydpi="61.120499"

74+ inkscape:export-xdpi="61.120499"

75+ xml:space="preserve"

77+ x="205"

78+ y="500.36218"

79+ id="text4178"

80+ sodipodi:linespacing="125%"><tspan

81+ id="tspan4180"

82+ sodipodi:role="line"

83+ x="205"

84+ y="500.36218"

86+ <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"

88+ d="m 200,484.3622 185,-1"

89+ id="path4182"

90+ inkscape:connector-curvature="0"

91+ inkscape:export-xdpi="61.120499"

92+ inkscape:export-ydpi="61.120499" />

93+ <path

94+ inkscape:connector-curvature="0"

95+ id="path4184"

96+ d="m 200,456.3622 185,-1"

97+ 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"

98+ inkscape:export-xdpi="61.120499"

99+ inkscape:export-ydpi="61.120499" />

100+ <text

101+ inkscape:export-ydpi="61.120499"

102+ inkscape:export-xdpi="61.120499"

103+ 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"

105+ x="229"

106+ y="447.36218"

107+ id="text4147"

108+ sodipodi:linespacing="125%"><tspan

109+ id="tspan4149"

110+ sodipodi:role="line"

111+ x="229"

112+ 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>

114+ </g>

115+</svg>

docs/image/elabLogicEx1_3.svgnew file+115

@@ -0,0 +1,115 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabLogicEx1_3.svg"

19+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"

20+ inkscape:export-xdpi="61.120499"

21+ inkscape:export-ydpi="61.120499">

22+ <defs

23+ id="defs4" />

24+ <sodipodi:namedview

25+ id="base"

26+ pagecolor="#ffffff"

27+ bordercolor="#666666"

28+ borderopacity="1.0"

29+ inkscape:pageopacity="0.0"

30+ inkscape:pageshadow="2"

31+ inkscape:zoom="1"

32+ inkscape:cx="425.25613"

33+ inkscape:cy="593.17666"

34+ inkscape:document-units="px"

35+ inkscape:current-layer="layer1"

36+ showgrid="false"

37+ inkscape:window-width="1175"

38+ inkscape:window-height="1011"

39+ inkscape:window-x="-4"

40+ inkscape:window-y="0"

41+ inkscape:window-maximized="0" />

42+ <metadata

43+ id="metadata7">

44+ <rdf:RDF>

45+ <cc:Work

46+ rdf:about="">

47+ <dc:format>image/svg+xml</dc:format>

48+ <dc:type

49+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

50+ <dc:title />

51+ </cc:Work>

52+ </rdf:RDF>

53+ </metadata>

54+ <g

55+ inkscape:label="Layer 1"

56+ inkscape:groupmode="layer"

57+ id="layer1">

58+ <text

59+ sodipodi:linespacing="125%"

60+ id="text4800"

61+ y="473.36218"

62+ x="205"

64+ xml:space="preserve"

65+ inkscape:export-xdpi="61.120499"

66+ 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'"

68+ y="473.36218"

69+ x="205"

70+ sodipodi:role="line"

71+ id="tspan4812">hole_2 : Nat</tspan></text>

72+ <text

73+ inkscape:export-ydpi="61.120499"

74+ inkscape:export-xdpi="61.120499"

75+ xml:space="preserve"

77+ x="205"

78+ y="500.36218"

79+ id="text4178"

80+ sodipodi:linespacing="125%"><tspan

81+ id="tspan4180"

82+ sodipodi:role="line"

83+ x="205"

84+ y="500.36218"

86+ <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"

88+ d="m 200,484.3622 185,-1"

89+ id="path4182"

90+ inkscape:connector-curvature="0"

91+ inkscape:export-xdpi="61.120499"

92+ inkscape:export-ydpi="61.120499" />

93+ <path

94+ inkscape:connector-curvature="0"

95+ id="path4184"

96+ d="m 200,456.3622 185,-1"

97+ 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"

98+ inkscape:export-xdpi="61.120499"

99+ inkscape:export-ydpi="61.120499" />

100+ <text

101+ inkscape:export-ydpi="61.120499"

102+ inkscape:export-xdpi="61.120499"

103+ xml:space="preserve"

105+ x="229"

106+ y="447.36218"

107+ id="text4147"

108+ sodipodi:linespacing="125%"><tspan

109+ id="tspan4149"

110+ sodipodi:role="line"

111+ x="229"

112+ 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>

114+ </g>

115+</svg>

docs/image/elabLogicEx1_4.svgnew file+80

@@ -0,0 +1,80 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabLogicEx1_4.svg"

19+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/elabLogicEx1_1.png"

20+ inkscape:export-xdpi="61.120499"

21+ inkscape:export-ydpi="61.120499">

22+ <defs

23+ id="defs4" />

24+ <sodipodi:namedview

25+ id="base"

26+ pagecolor="#ffffff"

27+ bordercolor="#666666"

28+ borderopacity="1.0"

29+ inkscape:pageopacity="0.0"

30+ inkscape:pageshadow="2"

31+ inkscape:zoom="1"

32+ inkscape:cx="425.25613"

33+ inkscape:cy="593.17666"

34+ inkscape:document-units="px"

35+ inkscape:current-layer="layer1"

36+ showgrid="false"

37+ inkscape:window-width="1157"

38+ inkscape:window-height="1011"

39+ inkscape:window-x="-4"

40+ inkscape:window-y="0"

41+ inkscape:window-maximized="0" />

42+ <metadata

43+ id="metadata7">

44+ <rdf:RDF>

45+ <cc:Work

46+ rdf:about="">

47+ <dc:format>image/svg+xml</dc:format>

48+ <dc:type

49+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

50+ <dc:title />

51+ </cc:Work>

52+ </rdf:RDF>

53+ </metadata>

54+ <g

55+ inkscape:label="Layer 1"

56+ inkscape:groupmode="layer"

57+ id="layer1">

58+ <text

59+ inkscape:export-ydpi="61.120499"

60+ inkscape:export-xdpi="61.120499"

61+ xml:space="preserve"

62+ 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"

63+ x="205"

64+ y="500.36218"

65+ id="text4178"

66+ sodipodi:linespacing="125%"><tspan

67+ id="tspan4180"

68+ sodipodi:role="line"

69+ x="205"

70+ y="500.36218"

71+ 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) -> Nat</tspan></text>

72+ <path

73+ 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"

74+ d="m 200,484.3622 185,-1"

75+ id="path4182"

76+ inkscape:connector-curvature="0"

77+ inkscape:export-xdpi="61.120499"

78+ inkscape:export-ydpi="61.120499" />

79+ </g>

80+</svg>

docs/image/elabProofState.svgnew file+356

@@ -0,0 +1,356 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabProofState.svg">

19+ <defs

20+ id="defs4" />

21+ <sodipodi:namedview

22+ id="base"

23+ pagecolor="#ffffff"

24+ bordercolor="#666666"

25+ borderopacity="1.0"

26+ inkscape:pageopacity="0.0"

27+ inkscape:pageshadow="2"

28+ inkscape:zoom="1"

29+ inkscape:cx="252.75613"

30+ inkscape:cy="520"

31+ inkscape:document-units="px"

32+ inkscape:current-layer="layer1"

33+ showgrid="false"

34+ inkscape:window-width="1920"

35+ inkscape:window-height="1015"

36+ inkscape:window-x="0"

37+ inkscape:window-y="0"

38+ inkscape:window-maximized="1" />

39+ <metadata

40+ id="metadata7">

41+ <rdf:RDF>

42+ <cc:Work

43+ rdf:about="">

44+ <dc:format>image/svg+xml</dc:format>

45+ <dc:type

46+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

47+ <dc:title />

48+ </cc:Work>

49+ </rdf:RDF>

50+ </metadata>

51+ <g

52+ inkscape:label="Layer 1"

53+ inkscape:groupmode="layer"

54+ id="layer1">

55+ <text

56+ sodipodi:linespacing="125%"

57+ id="text4148"

58+ y="330.36218"

59+ x="219"

60+ 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"

61+ xml:space="preserve"

62+ inkscape:export-xdpi="61.120499"

63+ inkscape:export-ydpi="61.120499"><tspan

64+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

65+ y="330.36218"

66+ x="219"

67+ id="tspan4150"

68+ sodipodi:role="line">current proof</tspan><tspan

69+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

70+ y="349.11218"

71+ x="219"

72+ sodipodi:role="line"

73+ id="tspan4206"> term</tspan></text>

74+ <text

75+ xml:space="preserve"

77+ x="240"

78+ y="303.36218"

79+ id="text4160"

80+ sodipodi:linespacing="125%"

81+ inkscape:export-xdpi="61.120499"

82+ inkscape:export-ydpi="61.120499"><tspan

83+ sodipodi:role="line"

84+ id="tspan4162"

85+ x="240"

86+ y="303.36218"

87+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">(TTName, TT)</tspan></text>

88+ <text

89+ sodipodi:linespacing="125%"

90+ id="text4202"

91+ y="392.36218"

92+ x="355"

93+ 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"

94+ xml:space="preserve"

95+ inkscape:export-xdpi="61.120499"

96+ inkscape:export-ydpi="61.120499"><tspan

97+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

98+ y="392.36218"

99+ x="355"

100+ id="tspan4204"

101+ sodipodi:role="line">original goal</tspan></text>

102+ <text

103+ xml:space="preserve"

105+ x="213"

106+ y="377.36218"

107+ id="text4208"

108+ sodipodi:linespacing="125%"

109+ inkscape:export-xdpi="61.120499"

110+ inkscape:export-ydpi="61.120499"><tspan

111+ id="tspan4212"

112+ sodipodi:role="line"

113+ x="213"

114+ y="377.36218"

115+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">path</tspan><tspan

116+ sodipodi:role="line"

117+ x="213"

118+ y="396.11218"

119+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

120+ id="tspan4216">subterm</tspan><tspan

121+ sodipodi:role="line"

122+ x="213"

123+ y="414.86218"

124+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

125+ id="tspan4218">updates</tspan></text>

126+ <text

127+ sodipodi:linespacing="125%"

128+ id="text4230"

129+ y="487.36218"

130+ x="148"

131+ 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"

132+ xml:space="preserve"

133+ inkscape:export-xdpi="61.120499"

134+ inkscape:export-ydpi="61.120499"><tspan

135+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

136+ y="487.36218"

137+ x="148"

138+ sodipodi:role="line"

139+ id="tspan4243">Contexts used for global definitions and for proof state.</tspan><tspan

140+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

141+ y="506.11218"

142+ x="148"

143+ sodipodi:role="line"

144+ id="tspan4190">They contain universe constraints and existing definitions.</tspan><tspan

145+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

146+ y="524.86218"

147+ x="148"

148+ sodipodi:role="line"

149+ id="tspan4253">Also store maximum RigCount of the namel</tspan></text>

150+ <text

151+ inkscape:export-ydpi="61.120499"

152+ inkscape:export-xdpi="61.120499"

153+ sodipodi:linespacing="125%"

154+ id="text4173"

155+ y="198.36218"

156+ x="135"

157+ 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"

158+ xml:space="preserve"><tspan

159+ 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"

160+ y="198.36218"

161+ x="135"

162+ id="tspan4175"

163+ sodipodi:role="line">Environment</tspan></text>

164+ <text

165+ xml:space="preserve"

166+ 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"

167+ x="350"

168+ y="197.36218"

169+ id="text4177"

170+ sodipodi:linespacing="125%"

171+ inkscape:export-xdpi="61.120499"

172+ inkscape:export-ydpi="61.120499"><tspan

173+ sodipodi:role="line"

174+ id="tspan4179"

175+ x="350"

176+ y="197.36218"

177+ 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">Holes</tspan></text>

178+ <text

179+ inkscape:export-ydpi="61.120499"

180+ inkscape:export-xdpi="61.120499"

181+ sodipodi:linespacing="125%"

182+ id="text4181"

183+ y="197.36218"

184+ x="460"

185+ 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"

186+ xml:space="preserve"><tspan

187+ 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"

188+ y="197.36218"

189+ x="460"

190+ id="tspan4183"

191+ sodipodi:role="line">Guess</tspan></text>

192+ <text

193+ inkscape:export-ydpi="61.120499"

194+ inkscape:export-xdpi="61.120499"

195+ sodipodi:linespacing="125%"

196+ id="text4185"

197+ y="199.36218"

198+ x="247"

199+ 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"

200+ xml:space="preserve"><tspan

201+ 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"

202+ y="199.36218"

203+ x="247"

204+ id="tspan4187"

205+ sodipodi:role="line">Goal</tspan></text>

206+ <rect

207+ 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"

208+ id="rect4189"

209+ width="95"

210+ height="32"

211+ x="134"

212+ y="205.3622"

213+ inkscape:export-xdpi="61.120499"

214+ inkscape:export-ydpi="61.120499" />

215+ <rect

216+ y="205.3622"

217+ x="241"

218+ height="32"

219+ width="95"

220+ id="rect4191"

221+ 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"

222+ inkscape:export-xdpi="61.120499"

223+ inkscape:export-ydpi="61.120499" />

224+ <rect

225+ 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"

226+ id="rect4195"

227+ width="95"

228+ height="32"

229+ x="454"

230+ y="205.3622"

231+ inkscape:export-xdpi="61.120499"

232+ inkscape:export-ydpi="61.120499" />

233+ <rect

234+ 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"

235+ id="rect4197"

236+ width="95"

237+ height="32"

238+ x="346"

239+ y="237.3622"

240+ inkscape:export-xdpi="61.120499"

241+ inkscape:export-ydpi="61.120499" />

242+ <rect

243+ y="269.36218"

244+ x="346"

245+ height="32"

246+ width="95"

247+ id="rect4199"

248+ 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"

249+ inkscape:export-xdpi="61.120499"

250+ inkscape:export-ydpi="61.120499" />

251+ <rect

252+ y="205.3622"

253+ x="346"

254+ height="32"

255+ width="95"

256+ id="rect4201"

257+ 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"

258+ inkscape:export-xdpi="61.120499"

259+ inkscape:export-ydpi="61.120499" />

260+ <path

261+ 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"

262+ d="m 169,242.3622 -9,184"

263+ id="path4206"

264+ inkscape:connector-curvature="0"

265+ inkscape:export-xdpi="61.120499"

266+ inkscape:export-ydpi="61.120499"

267+ sodipodi:nodetypes="cc" />

268+ <path

269+ inkscape:connector-curvature="0"

270+ id="path4208"

271+ d="m 301,240.3622 -26,46"

272+ 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"

273+ sodipodi:nodetypes="cc"

274+ inkscape:export-xdpi="61.120499"

275+ inkscape:export-ydpi="61.120499" />

276+ <text

277+ inkscape:export-ydpi="61.120499"

278+ inkscape:export-xdpi="61.120499"

279+ xml:space="preserve"

280+ 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"

281+ x="360"

282+ y="366.36218"

283+ id="text4210"

284+ sodipodi:linespacing="125%"><tspan

285+ sodipodi:role="line"

286+ id="tspan4213"

287+ x="360"

288+ y="366.36218"

289+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">focus</tspan></text>

290+ <rect

291+ inkscape:export-ydpi="61.120499"

292+ inkscape:export-xdpi="61.120499"

293+ y="237.3622"

294+ x="134"

295+ height="32"

296+ width="95"

297+ id="rect4747"

298+ 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" />

299+ <rect

300+ inkscape:export-ydpi="61.120499"

301+ inkscape:export-xdpi="61.120499"

302+ 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"

303+ id="rect4749"

304+ width="95"

305+ height="32"

306+ x="134"

307+ y="269.36218" />

308+ <text

309+ inkscape:export-ydpi="61.120499"

310+ inkscape:export-xdpi="61.120499"

311+ xml:space="preserve"

312+ 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"

313+ x="148"

314+ y="450.36218"

315+ id="text4751"

316+ sodipodi:linespacing="125%"><tspan

317+ id="tspan4757"

318+ sodipodi:role="line"

319+ x="148"

320+ y="450.36218"

321+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">List (TTName, Binder TT)</tspan><tspan

322+ sodipodi:role="line"

323+ x="148"

324+ y="469.11218"

325+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

326+ id="tspan4182">Open unification constaints.</tspan></text>

327+ <text

328+ inkscape:export-ydpi="61.120499"

329+ inkscape:export-xdpi="61.120499"

330+ xml:space="preserve"

331+ 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"

332+ x="349.25366"

333+ y="319.99084"

334+ id="text4210-3"

335+ sodipodi:linespacing="125%"><tspan

336+ sodipodi:role="line"

337+ id="tspan4213-6"

338+ x="349.25366"

339+ y="319.99084"

340+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">List TTName</tspan></text>

341+ <text

342+ sodipodi:linespacing="125%"

343+ id="text4782"

344+ y="251.99084"

345+ x="495.25366"

346+ 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"

347+ xml:space="preserve"

348+ inkscape:export-xdpi="61.120499"

349+ inkscape:export-ydpi="61.120499"><tspan

350+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

351+ y="251.99084"

352+ x="495.25366"

353+ id="tspan4784"

354+ sodipodi:role="line">TT</tspan></text>

355+ </g>

356+</svg>

docs/image/elabProofStateEx1_1.svgnew file+311

@@ -0,0 +1,311 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabProofStateEx1_1.svg">

19+ <defs

20+ id="defs4" />

21+ <sodipodi:namedview

22+ id="base"

23+ pagecolor="#ffffff"

24+ bordercolor="#666666"

25+ borderopacity="1.0"

26+ inkscape:pageopacity="0.0"

27+ inkscape:pageshadow="2"

28+ inkscape:zoom="1"

29+ inkscape:cx="425.25613"

30+ inkscape:cy="593.17666"

31+ inkscape:document-units="px"

32+ inkscape:current-layer="layer1"

33+ showgrid="false"

34+ inkscape:window-width="1920"

35+ inkscape:window-height="1015"

36+ inkscape:window-x="0"

37+ inkscape:window-y="0"

38+ inkscape:window-maximized="1" />

39+ <metadata

40+ id="metadata7">

41+ <rdf:RDF>

42+ <cc:Work

43+ rdf:about="">

44+ <dc:format>image/svg+xml</dc:format>

45+ <dc:type

46+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

47+ <dc:title />

48+ </cc:Work>

49+ </rdf:RDF>

50+ </metadata>

51+ <g

52+ inkscape:label="Layer 1"

53+ inkscape:groupmode="layer"

54+ id="layer1">

55+ <text

56+ sodipodi:linespacing="125%"

57+ id="text4140"

58+ y="226.36218"

59+ x="401"

61+ xml:space="preserve"

62+ inkscape:export-xdpi="61.120499"

63+ inkscape:export-ydpi="61.120499"><tspan

64+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

65+ y="226.36218"

66+ x="401"

67+ sodipodi:role="line"

68+ id="tspan4144">hole_2</tspan></text>

69+ <text

70+ inkscape:export-ydpi="61.120499"

71+ inkscape:export-xdpi="61.120499"

72+ sodipodi:linespacing="125%"

73+ id="text4173"

74+ y="198.36218"

75+ x="135"

77+ xml:space="preserve"><tspan

78+ 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"

79+ y="198.36218"

80+ x="135"

81+ id="tspan4175"

82+ sodipodi:role="line">Environment</tspan></text>

83+ <text

84+ xml:space="preserve"

85+ 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"

86+ x="393"

87+ y="197.36218"

88+ id="text4177"

89+ sodipodi:linespacing="125%"

90+ inkscape:export-xdpi="61.120499"

91+ inkscape:export-ydpi="61.120499"><tspan

92+ sodipodi:role="line"

93+ id="tspan4179"

94+ x="393"

95+ y="197.36218"

96+ 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">Holes</tspan></text>

97+ <text

98+ inkscape:export-ydpi="61.120499"

99+ inkscape:export-xdpi="61.120499"

100+ sodipodi:linespacing="125%"

101+ id="text4181"

102+ y="197.36218"

103+ x="503"

105+ xml:space="preserve"><tspan

106+ 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"

107+ y="197.36218"

108+ x="503"

109+ id="tspan4183"

110+ sodipodi:role="line">Guess</tspan></text>

111+ <text

112+ inkscape:export-ydpi="61.120499"

113+ inkscape:export-xdpi="61.120499"

114+ sodipodi:linespacing="125%"

115+ id="text4185"

116+ y="199.36218"

117+ x="247"

118+ 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"

119+ xml:space="preserve"><tspan

120+ 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"

121+ y="199.36218"

122+ x="247"

123+ id="tspan4187"

124+ sodipodi:role="line">Goal</tspan></text>

125+ <rect

126+ 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"

127+ id="rect4189"

128+ width="39"

129+ height="32"

130+ x="134"

131+ y="205.3622"

132+ inkscape:export-xdpi="61.120499"

133+ inkscape:export-ydpi="61.120499" />

134+ <rect

135+ y="206.3622"

136+ x="182"

137+ height="32"

138+ width="200"

139+ id="rect4191"

140+ 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"

141+ inkscape:export-xdpi="61.120499"

142+ inkscape:export-ydpi="61.120499" />

143+ <rect

144+ 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"

145+ id="rect4195"

146+ width="95"

147+ height="32"

148+ x="494"

149+ y="206.3622"

150+ inkscape:export-xdpi="61.120499"

151+ inkscape:export-ydpi="61.120499" />

152+ <rect

153+ 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"

154+ id="rect4197"

155+ width="95"

156+ height="32"

157+ x="389"

158+ y="237.3622"

159+ inkscape:export-xdpi="61.120499"

160+ inkscape:export-ydpi="61.120499" />

161+ <rect

162+ y="269.36218"

163+ x="389"

164+ height="32"

165+ width="95"

166+ id="rect4199"

167+ 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"

168+ inkscape:export-xdpi="61.120499"

169+ inkscape:export-ydpi="61.120499" />

170+ <rect

171+ y="205.3622"

172+ x="389"

173+ height="32"

174+ width="95"

175+ id="rect4201"

176+ 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"

177+ inkscape:export-xdpi="61.120499"

178+ inkscape:export-ydpi="61.120499" />

179+ <text

180+ inkscape:export-ydpi="61.120499"

181+ inkscape:export-xdpi="61.120499"

182+ xml:space="preserve"

183+ 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"

184+ x="400"

185+ y="257.36218"

186+ id="text4276"

187+ sodipodi:linespacing="125%"><tspan

188+ id="tspan4280"

189+ sodipodi:role="line"

190+ x="400"

191+ y="257.36218"

192+ 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</tspan></text>

193+ <text

194+ sodipodi:linespacing="125%"

195+ id="text4159"

196+ y="225.36218"

197+ x="141"

198+ 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"

199+ xml:space="preserve"

200+ inkscape:export-xdpi="61.120499"

201+ inkscape:export-ydpi="61.120499"><tspan

202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

203+ y="225.36218"

204+ x="141"

205+ sodipodi:role="line"

206+ id="tspan4161">[ ]</tspan></text>

207+ <text

208+ sodipodi:linespacing="125%"

209+ id="text4163"

210+ y="315.36218"

211+ x="171"

212+ 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"

213+ xml:space="preserve"

214+ inkscape:export-xdpi="61.120499"

215+ inkscape:export-ydpi="61.120499"><tspan

216+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

217+ y="315.36218"

218+ x="171"

219+ sodipodi:role="line"

220+ id="tspan4165">starts off empty</tspan></text>

221+ <path

222+ 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"

223+ d="m 157,223.3622 11,88"

224+ id="path4167"

225+ inkscape:connector-curvature="0"

226+ inkscape:export-xdpi="61.120499"

227+ inkscape:export-ydpi="61.120499" />

228+ <text

229+ inkscape:export-ydpi="61.120499"

230+ inkscape:export-xdpi="61.120499"

231+ xml:space="preserve"

232+ 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"

233+ x="188"

234+ y="227.36218"

235+ id="text4786"

236+ sodipodi:linespacing="125%"><tspan

237+ sodipodi:role="line"

238+ x="188"

239+ y="227.36218"

240+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

241+ id="tspan4790">(hole_2 , pi_arg : Nat->Nat)</tspan></text>

242+ <text

243+ inkscape:export-ydpi="61.120499"

244+ inkscape:export-xdpi="61.120499"

245+ xml:space="preserve"

246+ 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"

247+ x="240"

248+ y="345.36218"

249+ id="text4794"

250+ sodipodi:linespacing="125%"><tspan

251+ id="tspan4796"

252+ sodipodi:role="line"

253+ x="240"

254+ y="345.36218"

255+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">this is the signature</tspan><tspan

256+ sodipodi:role="line"

257+ x="240"

258+ y="364.11218"

259+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

260+ id="tspan4810">we are looking for</tspan></text>

261+ <path

262+ inkscape:connector-curvature="0"

263+ id="path4798"

264+ d="m 298,236.3622 9,98"

265+ 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"

266+ sodipodi:nodetypes="cc"

267+ inkscape:export-xdpi="61.120499"

268+ inkscape:export-ydpi="61.120499" />

269+ <text

270+ sodipodi:linespacing="125%"

271+ id="text4800"

272+ y="350.36218"

273+ x="404"

274+ 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"

275+ xml:space="preserve"

276+ inkscape:export-xdpi="61.120499"

277+ inkscape:export-ydpi="61.120499"><tspan

278+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

279+ y="350.36218"

280+ x="404"

281+ sodipodi:role="line"

282+ id="tspan4802">machine chosen</tspan><tspan

283+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

284+ y="369.11218"

285+ x="404"

286+ sodipodi:role="line"

287+ id="tspan4812">names for the holes</tspan></text>

288+ <path

289+ sodipodi:nodetypes="cc"

290+ 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"

291+ d="m 432,265.3622 8,68"

292+ id="path4804"

293+ inkscape:connector-curvature="0"

294+ inkscape:export-xdpi="61.120499"

295+ inkscape:export-ydpi="61.120499" />

296+ <text

297+ inkscape:export-ydpi="61.120499"

298+ inkscape:export-xdpi="61.120499"

299+ xml:space="preserve"

300+ 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"

301+ x="498"

302+ y="227.36218"

303+ id="text4806"

304+ sodipodi:linespacing="125%"><tspan

305+ id="tspan4808"

306+ sodipodi:role="line"

307+ x="498"

308+ y="227.36218"

309+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">no guess yet</tspan></text>

310+ </g>

311+</svg>

docs/image/elabProofStateEx1_2.svgnew file+271

@@ -0,0 +1,271 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabProofStateEx1_2.svg">

19+ <defs

20+ id="defs4" />

21+ <sodipodi:namedview

22+ id="base"

23+ pagecolor="#ffffff"

24+ bordercolor="#666666"

25+ borderopacity="1.0"

26+ inkscape:pageopacity="0.0"

27+ inkscape:pageshadow="2"

28+ inkscape:zoom="1"

29+ inkscape:cx="211.75967"

30+ inkscape:cy="688.76752"

31+ inkscape:document-units="px"

32+ inkscape:current-layer="layer1"

33+ showgrid="false"

34+ inkscape:window-width="1920"

35+ inkscape:window-height="1015"

36+ inkscape:window-x="0"

37+ inkscape:window-y="0"

38+ inkscape:window-maximized="1" />

39+ <metadata

40+ id="metadata7">

41+ <rdf:RDF>

42+ <cc:Work

43+ rdf:about="">

44+ <dc:format>image/svg+xml</dc:format>

45+ <dc:type

46+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

47+ <dc:title />

48+ </cc:Work>

49+ </rdf:RDF>

50+ </metadata>

51+ <g

52+ inkscape:label="Layer 1"

53+ inkscape:groupmode="layer"

54+ id="layer1">

55+ <text

56+ sodipodi:linespacing="125%"

57+ id="text4140"

58+ y="226.36218"

59+ x="401"

61+ xml:space="preserve"

62+ inkscape:export-xdpi="61.120499"

63+ inkscape:export-ydpi="61.120499"><tspan

64+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

65+ y="226.36218"

66+ x="401"

67+ sodipodi:role="line"

68+ id="tspan4144">hole_2</tspan></text>

69+ <text

70+ inkscape:export-ydpi="61.120499"

71+ inkscape:export-xdpi="61.120499"

72+ sodipodi:linespacing="125%"

73+ id="text4173"

74+ y="198.36218"

75+ x="135"

77+ xml:space="preserve"><tspan

78+ 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"

79+ y="198.36218"

80+ x="135"

81+ id="tspan4175"

82+ sodipodi:role="line">Environment</tspan></text>

83+ <text

84+ xml:space="preserve"

86+ x="393"

87+ y="197.36218"

88+ id="text4177"

89+ sodipodi:linespacing="125%"

90+ inkscape:export-xdpi="61.120499"

91+ inkscape:export-ydpi="61.120499"><tspan

92+ sodipodi:role="line"

93+ id="tspan4179"

94+ x="393"

95+ y="197.36218"

97+ <text

98+ inkscape:export-ydpi="61.120499"

99+ inkscape:export-xdpi="61.120499"

100+ sodipodi:linespacing="125%"

101+ id="text4181"

102+ y="197.36218"

103+ x="503"

105+ xml:space="preserve"><tspan

106+ 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"

107+ y="197.36218"

108+ x="503"

109+ id="tspan4183"

110+ sodipodi:role="line">Guess</tspan></text>

111+ <text

112+ inkscape:export-ydpi="61.120499"

113+ inkscape:export-xdpi="61.120499"

114+ sodipodi:linespacing="125%"

115+ id="text4185"

116+ y="199.36218"

117+ x="247"

119+ xml:space="preserve"><tspan

120+ 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"

121+ y="199.36218"

122+ x="247"

123+ id="tspan4187"

124+ sodipodi:role="line">Goal</tspan></text>

125+ <rect

126+ 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"

127+ id="rect4189"

128+ width="92"

129+ height="32"

130+ x="134"

131+ y="205.3622"

132+ inkscape:export-xdpi="61.120499"

133+ inkscape:export-ydpi="61.120499" />

134+ <rect

135+ y="206.3622"

136+ x="234"

137+ height="32"

138+ width="148"

139+ id="rect4191"

140+ 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"

141+ inkscape:export-xdpi="61.120499"

142+ inkscape:export-ydpi="61.120499" />

143+ <rect

144+ 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"

145+ id="rect4195"

146+ width="95"

147+ height="32"

148+ x="497"

149+ y="205.3622"

150+ inkscape:export-xdpi="61.120499"

151+ inkscape:export-ydpi="61.120499" />

152+ <rect

153+ 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"

154+ id="rect4197"

155+ width="95"

156+ height="32"

157+ x="389"

158+ y="237.3622"

159+ inkscape:export-xdpi="61.120499"

160+ inkscape:export-ydpi="61.120499" />

161+ <rect

162+ y="269.36218"

163+ x="389"

164+ height="32"

165+ width="95"

166+ id="rect4199"

167+ 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"

168+ inkscape:export-xdpi="61.120499"

169+ inkscape:export-ydpi="61.120499" />

170+ <rect

171+ y="205.3622"

172+ x="389"

173+ height="32"

174+ width="95"

175+ id="rect4201"

176+ 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"

177+ inkscape:export-xdpi="61.120499"

178+ inkscape:export-ydpi="61.120499" />

179+ <text

180+ inkscape:export-ydpi="61.120499"

181+ inkscape:export-xdpi="61.120499"

182+ xml:space="preserve"

184+ x="400"

185+ y="257.36218"

186+ id="text4276"

187+ sodipodi:linespacing="125%"><tspan

188+ id="tspan4280"

189+ sodipodi:role="line"

190+ x="400"

191+ y="257.36218"

192+ 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</tspan></text>

193+ <text

194+ sodipodi:linespacing="125%"

195+ id="text4159"

196+ y="225.36218"

197+ x="140"

199+ xml:space="preserve"

200+ inkscape:export-xdpi="61.120499"

201+ inkscape:export-ydpi="61.120499"><tspan

202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

203+ y="225.36218"

204+ x="140"

205+ sodipodi:role="line"

206+ id="tspan4161">(x, λ Nat)</tspan></text>

207+ <text

208+ inkscape:export-ydpi="61.120499"

209+ inkscape:export-xdpi="61.120499"

210+ xml:space="preserve"

211+ 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"

212+ x="266"

213+ y="226.36218"

214+ id="text4786"

215+ sodipodi:linespacing="125%"><tspan

216+ sodipodi:role="line"

217+ x="266"

218+ y="226.36218"

219+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

220+ id="tspan4790">(hole_2 , Nat)</tspan></text>

221+ <path

222+ inkscape:connector-curvature="0"

223+ id="path4798"

224+ d="m 298,236.3622 9,98"

225+ 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"

226+ sodipodi:nodetypes="cc"

227+ inkscape:export-xdpi="61.120499"

228+ inkscape:export-ydpi="61.120499" />

229+ <text

230+ sodipodi:linespacing="125%"

231+ id="text4800"

232+ y="350.36218"

233+ x="404"

234+ 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"

235+ xml:space="preserve"

236+ inkscape:export-xdpi="61.120499"

237+ inkscape:export-ydpi="61.120499"><tspan

238+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

239+ y="350.36218"

240+ x="404"

241+ sodipodi:role="line"

242+ id="tspan4802">machine chosen</tspan><tspan

243+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

244+ y="369.11218"

245+ x="404"

246+ sodipodi:role="line"

247+ id="tspan4812">names for the holes</tspan></text>

248+ <path

249+ sodipodi:nodetypes="cc"

250+ 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"

251+ d="m 432,265.3622 8,68"

252+ id="path4804"

253+ inkscape:connector-curvature="0"

254+ inkscape:export-xdpi="61.120499"

255+ inkscape:export-ydpi="61.120499" />

256+ <text

257+ inkscape:export-ydpi="61.120499"

258+ inkscape:export-xdpi="61.120499"

259+ xml:space="preserve"

260+ 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"

261+ x="510"

262+ y="226.36218"

263+ id="text4174"

264+ sodipodi:linespacing="125%"><tspan

265+ id="tspan4176"

266+ sodipodi:role="line"

267+ x="510"

268+ y="226.36218"

269+ 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>

270+ </g>

271+</svg>

docs/image/elabProofStateEx1_3.svgnew file+274

@@ -0,0 +1,274 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="elabProofStateEx1_3.svg"

19+ inkscape:export-filename="/home/master/euclid/prog/idris/elaborator/elabTactics/example1/elabProofStateEx1_3.png"

20+ inkscape:export-xdpi="61.120499"

21+ inkscape:export-ydpi="61.120499">

22+ <defs

23+ id="defs4" />

24+ <sodipodi:namedview

25+ id="base"

26+ pagecolor="#ffffff"

27+ bordercolor="#666666"

28+ borderopacity="1.0"

29+ inkscape:pageopacity="0.0"

30+ inkscape:pageshadow="2"

31+ inkscape:zoom="1"

32+ inkscape:cx="345.95856"

33+ inkscape:cy="688.76752"

34+ inkscape:document-units="px"

35+ inkscape:current-layer="layer1"

36+ showgrid="false"

37+ inkscape:window-width="1920"

38+ inkscape:window-height="1015"

39+ inkscape:window-x="0"

40+ inkscape:window-y="0"

41+ inkscape:window-maximized="1" />

42+ <metadata

43+ id="metadata7">

44+ <rdf:RDF>

45+ <cc:Work

46+ rdf:about="">

47+ <dc:format>image/svg+xml</dc:format>

48+ <dc:type

49+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

50+ <dc:title />

51+ </cc:Work>

52+ </rdf:RDF>

53+ </metadata>

54+ <g

55+ inkscape:label="Layer 1"

56+ inkscape:groupmode="layer"

57+ id="layer1">

58+ <text

59+ sodipodi:linespacing="125%"

60+ id="text4140"

61+ y="226.36218"

62+ x="401"

64+ xml:space="preserve"

65+ inkscape:export-xdpi="61.120499"

66+ 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'"

68+ y="226.36218"

69+ x="401"

70+ sodipodi:role="line"

71+ id="tspan4144">hole_2</tspan></text>

72+ <text

73+ inkscape:export-ydpi="61.120499"

74+ inkscape:export-xdpi="61.120499"

75+ sodipodi:linespacing="125%"

76+ id="text4173"

77+ y="198.36218"

78+ x="135"

79+ 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"

80+ xml:space="preserve"><tspan

81+ 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"

82+ y="198.36218"

83+ x="135"

84+ id="tspan4175"

85+ sodipodi:role="line">Environment</tspan></text>

86+ <text

87+ xml:space="preserve"

88+ 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"

89+ x="393"

90+ y="197.36218"

91+ id="text4177"

92+ sodipodi:linespacing="125%"

93+ inkscape:export-xdpi="61.120499"

94+ inkscape:export-ydpi="61.120499"><tspan

95+ sodipodi:role="line"

96+ id="tspan4179"

97+ x="393"

98+ y="197.36218"

99+ 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">Holes</tspan></text>

100+ <text

101+ inkscape:export-ydpi="61.120499"

102+ inkscape:export-xdpi="61.120499"

103+ sodipodi:linespacing="125%"

104+ id="text4181"

105+ y="197.36218"

106+ x="503"

107+ 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"

108+ xml:space="preserve"><tspan

109+ 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"

110+ y="197.36218"

111+ x="503"

112+ id="tspan4183"

113+ sodipodi:role="line">Guess</tspan></text>

114+ <text

115+ inkscape:export-ydpi="61.120499"

116+ inkscape:export-xdpi="61.120499"

117+ sodipodi:linespacing="125%"

118+ id="text4185"

119+ y="199.36218"

120+ x="247"

121+ 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"

122+ xml:space="preserve"><tspan

123+ 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"

124+ y="199.36218"

125+ x="247"

126+ id="tspan4187"

127+ sodipodi:role="line">Goal</tspan></text>

128+ <rect

129+ 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"

130+ id="rect4189"

131+ width="92"

132+ height="32"

133+ x="134"

134+ y="205.3622"

135+ inkscape:export-xdpi="61.120499"

136+ inkscape:export-ydpi="61.120499" />

137+ <rect

138+ y="206.3622"

139+ x="234"

140+ height="32"

141+ width="148"

142+ id="rect4191"

143+ 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"

144+ inkscape:export-xdpi="61.120499"

145+ inkscape:export-ydpi="61.120499" />

146+ <rect

147+ 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"

148+ id="rect4195"

149+ width="95"

150+ height="32"

151+ x="497"

152+ y="205.3622"

153+ inkscape:export-xdpi="61.120499"

154+ inkscape:export-ydpi="61.120499" />

155+ <rect

156+ 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"

157+ id="rect4197"

158+ width="95"

159+ height="32"

160+ x="389"

161+ y="237.3622"

162+ inkscape:export-xdpi="61.120499"

163+ inkscape:export-ydpi="61.120499" />

164+ <rect

165+ y="269.36218"

166+ x="389"

167+ height="32"

168+ width="95"

169+ id="rect4199"

170+ 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"

171+ inkscape:export-xdpi="61.120499"

172+ inkscape:export-ydpi="61.120499" />

173+ <rect

174+ y="205.3622"

175+ x="389"

176+ height="32"

177+ width="95"

178+ id="rect4201"

179+ 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"

180+ inkscape:export-xdpi="61.120499"

181+ inkscape:export-ydpi="61.120499" />

182+ <text

183+ inkscape:export-ydpi="61.120499"

184+ inkscape:export-xdpi="61.120499"

185+ xml:space="preserve"

186+ 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"

187+ x="400"

188+ y="257.36218"

189+ id="text4276"

190+ sodipodi:linespacing="125%"><tspan

191+ id="tspan4280"

192+ sodipodi:role="line"

193+ x="400"

194+ y="257.36218"

195+ 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</tspan></text>

196+ <text

197+ sodipodi:linespacing="125%"

198+ id="text4159"

199+ y="225.36218"

200+ x="140"

201+ 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"

202+ xml:space="preserve"

203+ inkscape:export-xdpi="61.120499"

204+ inkscape:export-ydpi="61.120499"><tspan

205+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

206+ y="225.36218"

207+ x="140"

208+ sodipodi:role="line"

209+ id="tspan4161">(x, λ Nat)</tspan></text>

210+ <text

211+ inkscape:export-ydpi="61.120499"

212+ inkscape:export-xdpi="61.120499"

213+ xml:space="preserve"

214+ 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"

215+ x="266"

216+ y="226.36218"

217+ id="text4786"

218+ sodipodi:linespacing="125%"><tspan

219+ sodipodi:role="line"

220+ x="266"

221+ y="226.36218"

222+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

223+ id="tspan4790">(hole_2 , Nat)</tspan></text>

224+ <path

225+ inkscape:connector-curvature="0"

226+ id="path4798"

227+ d="m 298,236.3622 9,98"

228+ 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"

229+ sodipodi:nodetypes="cc"

230+ inkscape:export-xdpi="61.120499"

231+ inkscape:export-ydpi="61.120499" />

232+ <text

233+ sodipodi:linespacing="125%"

234+ id="text4800"

235+ y="350.36218"

236+ x="404"

237+ 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"

238+ xml:space="preserve"

239+ inkscape:export-xdpi="61.120499"

240+ inkscape:export-ydpi="61.120499"><tspan

241+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

242+ y="350.36218"

243+ x="404"

244+ sodipodi:role="line"

245+ id="tspan4802">machine chosen</tspan><tspan

246+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

247+ y="369.11218"

248+ x="404"

249+ sodipodi:role="line"

250+ id="tspan4812">names for the holes</tspan></text>

251+ <path

252+ sodipodi:nodetypes="cc"

253+ 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"

254+ d="m 432,265.3622 8,68"

255+ id="path4804"

256+ inkscape:connector-curvature="0"

257+ inkscape:export-xdpi="61.120499"

258+ inkscape:export-ydpi="61.120499" />

259+ <text

260+ inkscape:export-ydpi="61.120499"

261+ inkscape:export-xdpi="61.120499"

262+ xml:space="preserve"

263+ 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"

264+ x="510"

265+ y="226.36218"

266+ id="text4174"

267+ sodipodi:linespacing="125%"><tspan

268+ id="tspan4176"

269+ sodipodi:role="line"

270+ x="510"

271+ y="226.36218"

272+ 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>

273+ </g>

274+</svg>

docs/image/idrisTopLevel.png

Binary file not shown.

docs/image/idrisTopLevel.svgnew file+524

@@ -0,0 +1,524 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="idrisTopLevel.svg">

19+ <defs

20+ id="defs4">

21+ <marker

22+ inkscape:stockid="Arrow1Mend"

23+ orient="auto"

24+ refY="0.0"

25+ refX="0.0"

26+ id="marker4198"

27+ style="overflow:visible;"

28+ inkscape:isstock="true">

29+ <path

30+ id="path4200"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="marker4203"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="path4205" />

49+ </marker>

50+ <marker

51+ inkscape:stockid="Arrow1Mend"

52+ orient="auto"

53+ refY="0.0"

54+ refX="0.0"

55+ id="marker4197"

56+ style="overflow:visible;"

57+ inkscape:isstock="true"

58+ inkscape:collect="always">

59+ <path

60+ id="path4199"

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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

63+ transform="scale(0.4) rotate(180) translate(10,0)" />

64+ </marker>

65+ <marker

66+ inkscape:stockid="Arrow1Mend"

67+ orient="auto"

68+ refY="0.0"

69+ refX="0.0"

70+ id="marker4182"

71+ style="overflow:visible;"

72+ inkscape:isstock="true">

73+ <path

74+ id="path4184"

75+ 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 "

76+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

77+ transform="scale(0.4) rotate(180) translate(10,0)" />

78+ </marker>

79+ <marker

80+ inkscape:isstock="true"

81+ style="overflow:visible;"

82+ id="marker4176"

83+ refX="0.0"

84+ refY="0.0"

85+ orient="auto"

86+ inkscape:stockid="Arrow1Mend"

87+ inkscape:collect="always">

88+ <path

89+ transform="scale(0.4) rotate(180) translate(10,0)"

90+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

91+ 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 "

92+ id="path4178" />

93+ </marker>

94+ <marker

95+ inkscape:stockid="Arrow1Mend"

96+ orient="auto"

97+ refY="0.0"

98+ refX="0.0"

99+ id="marker4830"

100+ style="overflow:visible;"

101+ inkscape:isstock="true"

102+ inkscape:collect="always">

103+ <path

104+ id="path4832"

105+ 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 "

106+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

107+ transform="scale(0.4) rotate(180) translate(10,0)" />

108+ </marker>

109+ <marker

110+ inkscape:stockid="Arrow1Mend"

111+ orient="auto"

112+ refY="0.0"

113+ refX="0.0"

114+ id="Arrow1Mend"

115+ style="overflow:visible;"

116+ inkscape:isstock="true"

117+ inkscape:collect="always">

118+ <path

119+ id="path4175"

120+ 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 "

121+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

122+ transform="scale(0.4) rotate(180) translate(10,0)" />

123+ </marker>

124+ </defs>

125+ <sodipodi:namedview

126+ id="base"

127+ pagecolor="#ffffff"

128+ bordercolor="#666666"

129+ borderopacity="1.0"

130+ inkscape:pageopacity="0.0"

131+ inkscape:pageshadow="2"

132+ inkscape:zoom="1"

133+ inkscape:cx="353.5"

134+ inkscape:cy="669.5"

135+ inkscape:document-units="px"

136+ inkscape:current-layer="layer1"

137+ showgrid="false"

138+ inkscape:window-width="1744"

139+ inkscape:window-height="1011"

140+ inkscape:window-x="-4"

141+ inkscape:window-y="0"

142+ inkscape:window-maximized="0" />

143+ <metadata

144+ id="metadata7">

145+ <rdf:RDF>

146+ <cc:Work

147+ rdf:about="">

148+ <dc:format>image/svg+xml</dc:format>

149+ <dc:type

150+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

151+ <dc:title />

152+ </cc:Work>

153+ </rdf:RDF>

154+ </metadata>

155+ <g

156+ inkscape:label="Layer 1"

157+ inkscape:groupmode="layer"

158+ id="layer1">

159+ <text

160+ xml:space="preserve"

161+ style="font-style:normal;font-weight:normal;font-size:40px;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"

162+ x="21"

163+ y="411.36221"

164+ id="text4136"

165+ sodipodi:linespacing="125%"

166+ inkscape:export-xdpi="61.120499"

167+ inkscape:export-ydpi="61.120499"><tspan

168+ sodipodi:role="line"

169+ id="tspan4138"

170+ x="21"

171+ y="411.36221"

172+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000">Idris</tspan></text>

173+ <text

174+ sodipodi:linespacing="125%"

175+ id="text4140"

176+ y="411.36221"

177+ x="203"

178+ style="font-style:normal;font-weight:normal;font-size:40px;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"

179+ xml:space="preserve"

180+ inkscape:export-xdpi="61.120499"

181+ inkscape:export-ydpi="61.120499"><tspan

182+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000"

183+ y="411.36221"

184+ x="203"

185+ id="tspan4142"

186+ sodipodi:role="line">Idris</tspan></text>

187+ <text

188+ xml:space="preserve"

189+ style="font-style:normal;font-weight:normal;font-size:40px;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;"

190+ x="253"

191+ y="402.36218"

192+ id="text4144"

193+ sodipodi:linespacing="125%"

194+ inkscape:export-xdpi="61.120499"

195+ inkscape:export-ydpi="61.120499"><tspan

196+ sodipodi:role="line"

197+ id="tspan4146"

198+ x="253"

199+ y="402.36218"

200+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;">~</tspan></text>

201+ <text

202+ sodipodi:linespacing="125%"

203+ id="text4148"

204+ y="411.60635"

205+ x="451"

206+ style="font-style:normal;font-weight:normal;font-size:40px;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"

207+ xml:space="preserve"

208+ inkscape:export-xdpi="61.120499"

209+ inkscape:export-ydpi="61.120499"><tspan

210+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000"

211+ y="411.60635"

212+ x="451"

213+ id="tspan4150"

214+ sodipodi:role="line">TT</tspan></text>

215+ <text

216+ xml:space="preserve"

217+ style="font-style:normal;font-weight:normal;font-size:40px;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"

218+ x="610"

219+ y="411.36221"

220+ id="text4152"

221+ sodipodi:linespacing="125%"

222+ inkscape:export-xdpi="61.120499"

223+ inkscape:export-ydpi="61.120499"><tspan

224+ sodipodi:role="line"

225+ id="tspan4154"

226+ x="610"

227+ y="411.36221"

228+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000">Executable</tspan></text>

229+ <text

230+ sodipodi:linespacing="125%"

231+ id="text4156"

232+ y="436.36218"

233+ x="80"

234+ style="font-style:normal;font-weight:normal;font-size:40px;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"

235+ xml:space="preserve"

236+ inkscape:export-xdpi="61.120499"

237+ inkscape:export-ydpi="61.120499"><tspan

238+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

239+ y="436.36218"

240+ x="80"

241+ id="tspan4158"

242+ sodipodi:role="line">desugaring</tspan></text>

243+ <path

244+ 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;marker-end:url(#Arrow1Mend)"

245+ d="M 81.977612,407.11261 188,407.3622"

246+ id="path4160"

247+ inkscape:connector-curvature="0"

248+ inkscape:export-xdpi="61.120499"

249+ inkscape:export-ydpi="61.120499"

250+ sodipodi:nodetypes="cc" />

251+ <text

252+ xml:space="preserve"

253+ style="font-style:normal;font-weight:normal;font-size:40px;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"

254+ x="281"

255+ y="432.36218"

256+ id="text4790"

257+ sodipodi:linespacing="125%"

258+ inkscape:export-xdpi="61.120499"

259+ inkscape:export-ydpi="61.120499"><tspan

260+ sodipodi:role="line"

261+ id="tspan4792"

262+ x="281"

263+ y="432.36218"

264+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">elaboration</tspan></text>

265+ <text

266+ sodipodi:linespacing="125%"

267+ id="text4824"

268+ y="394.36218"

269+ x="498"

270+ style="font-style:normal;font-weight:normal;font-size:40px;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"

271+ xml:space="preserve"

272+ inkscape:export-xdpi="61.120499"

273+ inkscape:export-ydpi="61.120499"><tspan

274+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

275+ y="394.36218"

276+ x="498"

277+ id="tspan4826"

278+ sodipodi:role="line">compilation</tspan></text>

279+ <path

280+ 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;marker-end:url(#marker4830)"

281+ d="m 495,405.33981 105,0.0224"

282+ id="path4828"

283+ inkscape:connector-curvature="0"

284+ inkscape:export-xdpi="61.120499"

285+ inkscape:export-ydpi="61.120499"

286+ sodipodi:nodetypes="cc" />

287+ <text

288+ inkscape:export-ydpi="61.120499"

289+ inkscape:export-xdpi="61.120499"

290+ sodipodi:linespacing="125%"

291+ id="text4166"

292+ y="442.36218"

293+ x="609"

294+ style="font-style:normal;font-weight:normal;font-size:40px;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"

295+ xml:space="preserve"><tspan

296+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000"

297+ y="442.36218"

298+ x="609"

299+ id="tspan4168"

300+ sodipodi:role="line">C</tspan></text>

301+ <text

302+ xml:space="preserve"

303+ style="font-style:normal;font-weight:normal;font-size:40px;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"

304+ x="609"

305+ y="475.36218"

306+ id="text4170"

307+ sodipodi:linespacing="125%"

308+ inkscape:export-xdpi="61.120499"

309+ inkscape:export-ydpi="61.120499"><tspan

310+ sodipodi:role="line"

311+ id="tspan4172"

312+ x="609"

313+ y="475.36218"

314+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:25px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000">JS</tspan></text>

315+ <path

316+ inkscape:export-ydpi="61.120499"

317+ inkscape:export-xdpi="61.120499"

318+ inkscape:connector-curvature="0"

319+ id="path4174"

320+ d="m 495,406.3622 104,26"

321+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:8, 2;stroke-dashoffset:0;stroke-opacity:1;marker-end:url(#marker4176)"

322+ sodipodi:nodetypes="cc" />

323+ <path

324+ sodipodi:nodetypes="cc"

325+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:12, 2;stroke-dashoffset:0;stroke-opacity:1;marker-end:url(#marker4182)"

326+ d="M 495,405.90781 599,467.3622"

327+ id="path4180"

328+ inkscape:connector-curvature="0"

329+ inkscape:export-xdpi="61.120499"

330+ inkscape:export-ydpi="61.120499" />

331+ <text

332+ inkscape:export-ydpi="61.120499"

333+ inkscape:export-xdpi="61.120499"

334+ xml:space="preserve"

335+ 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"

336+ x="20"

337+ y="523.36218"

338+ id="text4186"

339+ sodipodi:linespacing="125%"><tspan

340+ sodipodi:role="line"

341+ x="20"

342+ y="523.36218"

343+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

344+ id="tspan4190">Add implicitly quantified variables.</tspan><tspan

345+ sodipodi:role="line"

346+ x="20"

347+ y="542.11218"

348+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

349+ id="tspan4191">Conditional expressions replaced by function calls.</tspan></text>

350+ <path

351+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"

352+ d="m 120.29902,440.01416 0.098,70.81863"

353+ id="path4192"

354+ inkscape:connector-curvature="0"

355+ inkscape:export-xdpi="61.120499"

356+ inkscape:export-ydpi="61.120499"

357+ sodipodi:nodetypes="cc" />

358+ <text

359+ sodipodi:linespacing="125%"

360+ id="text4194"

361+ y="367.36218"

362+ x="358"

363+ 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"

364+ xml:space="preserve"

365+ inkscape:export-xdpi="61.120499"

366+ inkscape:export-ydpi="61.120499"><tspan

367+ id="tspan4198"

368+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

369+ y="367.36218"

370+ x="358"

371+ sodipodi:role="line">proof tactics</tspan></text>

372+ <path

373+ inkscape:connector-curvature="0"

374+ id="path4202"

375+ d="m 382.73881,368.53384 0.16418,32.3209"

376+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"

377+ sodipodi:nodetypes="cc"

378+ inkscape:export-xdpi="61.120499"

379+ inkscape:export-ydpi="61.120499" />

380+ <path

381+ inkscape:export-ydpi="61.120499"

382+ inkscape:export-xdpi="61.120499"

383+ 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;marker-end:url(#marker4197)"

384+ d="m 277,403.3622 37.7728,-0.0912"

385+ id="path4195"

386+ inkscape:connector-curvature="0"

387+ sodipodi:nodetypes="cc" />

388+ <path

389+ sodipodi:nodetypes="cc"

390+ inkscape:connector-curvature="0"

391+ id="path4201"

392+ d="m 335,403.15739 37.8864,-0.31841"

393+ 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;marker-end:url(#marker4203)"

394+ inkscape:export-xdpi="61.120499"

395+ inkscape:export-ydpi="61.120499" />

396+ <text

397+ inkscape:export-ydpi="61.120499"

398+ inkscape:export-xdpi="61.120499"

399+ xml:space="preserve"

400+ 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"

401+ x="215"

402+ y="340.36218"

403+ id="text4207"

404+ sodipodi:linespacing="125%"><tspan

405+ sodipodi:role="line"

406+ x="215"

407+ y="340.36218"

408+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

409+ id="tspan4209">during elaboration</tspan><tspan

410+ sodipodi:role="line"

411+ x="215"

412+ y="359.11218"

413+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

414+ id="tspan4213">may contain holes</tspan><tspan

415+ sodipodi:role="line"

416+ x="215"

417+ y="377.86218"

418+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

419+ id="tspan4199">and guesses</tspan></text>

420+ <path

421+ inkscape:export-ydpi="61.120499"

422+ inkscape:export-xdpi="61.120499"

423+ sodipodi:nodetypes="cc"

424+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"

425+ d="m 324,399.3622 0.11194,-38.03731"

426+ id="path4211"

427+ inkscape:connector-curvature="0" />

428+ <text

429+ sodipodi:linespacing="125%"

430+ id="text4215"

431+ y="461.36218"

432+ x="233"

433+ 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"

434+ xml:space="preserve"

435+ inkscape:export-xdpi="61.120499"

436+ inkscape:export-ydpi="61.120499"><tspan

437+ id="tspan4217"

438+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

439+ y="461.36218"

440+ x="233"

441+ sodipodi:role="line">Make explicit all types.</tspan><tspan

442+ id="tspan4223"

443+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

444+ y="480.11218"

445+ x="233"

446+ sodipodi:role="line">Make explicit function and </tspan><tspan

447+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

448+ y="498.86218"

449+ x="233"

450+ sodipodi:role="line"

451+ id="tspan4235"> pattern match variables.</tspan></text>

452+ <path

453+ inkscape:export-ydpi="61.120499"

454+ inkscape:export-xdpi="61.120499"

455+ sodipodi:nodetypes="cc"

456+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"

457+ d="m 323.7402,434.372 0.0637,16.14706"

458+ id="path4237"

459+ inkscape:connector-curvature="0" />

460+ <path

461+ inkscape:export-ydpi="61.120499"

462+ inkscape:export-xdpi="61.120499"

463+ 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;marker-end:url(#marker4198)"

464+ d="m 395,402.49819 45.38391,-0.31841"

465+ id="path4196"

466+ inkscape:connector-curvature="0"

467+ sodipodi:nodetypes="cc" />

468+ <text

469+ inkscape:export-ydpi="61.120499"

470+ inkscape:export-xdpi="61.120499"

471+ xml:space="preserve"

472+ 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"

473+ x="431"

474+ y="465.36218"

475+ id="text4202"

476+ sodipodi:linespacing="125%"><tspan

477+ sodipodi:role="line"

478+ x="431"

479+ y="465.36218"

480+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

481+ id="tspan4204">type checker</tspan><tspan

482+ sodipodi:role="line"

483+ x="431"

484+ y="484.11218"

485+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"

486+ id="tspan4208">Raw -> TT</tspan></text>

487+ <path

488+ inkscape:export-ydpi="61.120499"

489+ inkscape:export-xdpi="61.120499"

490+ sodipodi:nodetypes="cc"

491+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"

492+ d="m 421,411.3622 39,40"

493+ id="path4206"

494+ inkscape:connector-curvature="0" />

495+ <text

496+ inkscape:export-ydpi="61.120499"

497+ inkscape:export-xdpi="61.120499"

498+ xml:space="preserve"

499+ style="font-style:normal;font-weight:normal;font-size:40px;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"

500+ x="378"

501+ y="417.36218"

502+ id="text4203"

503+ sodipodi:linespacing="125%"><tspan

504+ sodipodi:role="line"

505+ id="tspan4205"

506+ x="378"

507+ y="417.36218"

508+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000">Raw</tspan></text>

509+ <text

510+ sodipodi:linespacing="125%"

511+ id="text4205"

512+ y="432.36218"

513+ x="201"

514+ style="font-style:normal;font-weight:normal;font-size:40px;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"

515+ xml:space="preserve"

516+ inkscape:export-xdpi="61.120499"

517+ inkscape:export-ydpi="61.120499"><tspan

518+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:15px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000"

519+ y="432.36218"

520+ x="201"

521+ id="tspan4207"

522+ sodipodi:role="line">PTerm</tspan></text>

523+ </g>

524+</svg>

docs/image/tree.svgnew file+180

@@ -0,0 +1,180 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

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="tree.svg">

19+ <defs

20+ id="defs4">

21+ <marker

22+ inkscape:isstock="true"

23+ style="overflow:visible;"

24+ id="marker5204"

25+ refX="0.0"

26+ refY="0.0"

27+ orient="auto"

28+ inkscape:stockid="Arrow1Mend">

29+ <path

30+ transform="scale(0.4) rotate(180) translate(10,0)"

31+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

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" />

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>

51+ <sodipodi:namedview

52+ id="base"

53+ pagecolor="#ffffff"

54+ bordercolor="#666666"

55+ borderopacity="1.0"

56+ inkscape:pageopacity="0.0"

57+ inkscape:pageshadow="2"

58+ inkscape:zoom="1"

59+ inkscape:cx="383.03443"

60+ inkscape:cy="520"

61+ inkscape:document-units="px"

62+ inkscape:current-layer="layer1"

63+ showgrid="false"

64+ inkscape:window-width="1406"

65+ inkscape:window-height="1011"

66+ inkscape:window-x="-4"

67+ inkscape:window-y="0"

68+ inkscape:window-maximized="0" />

69+ <metadata

70+ id="metadata7">

71+ <rdf:RDF>

72+ <cc:Work

73+ rdf:about="">

74+ <dc:format>image/svg+xml</dc:format>

75+ <dc:type

76+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

77+ <dc:title></dc:title>

78+ </cc:Work>

79+ </rdf:RDF>

80+ </metadata>

81+ <g

82+ inkscape:label="Layer 1"

83+ inkscape:groupmode="layer"

84+ id="layer1">

85+ <text

86+ 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"

88+ x="221"

89+ y="433.36221"

90+ id="text4136"

91+ sodipodi:linespacing="125%"

92+ inkscape:export-xdpi="61.120499"

93+ inkscape:export-ydpi="61.120499"><tspan

94+ sodipodi:role="line"

95+ id="tspan4138"

96+ x="221"

97+ y="433.36221"

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>

99+ <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"

124+ y="466.36221"

125+ x="161"

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"

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-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;fill-opacity:1"

131+ y="466.36221"

132+ x="161"

133+ id="tspan4154"

134+ sodipodi:role="line">intro `{{x}}</tspan></text>

135+ <text

136+ 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"

138+ x="322"

139+ y="468.36221"

140+ id="text4156"

141+ sodipodi:linespacing="125%"

142+ inkscape:export-xdpi="61.120499"

143+ inkscape:export-ydpi="61.120499"><tspan

144+ sodipodi:role="line"

145+ id="tspan4158"

146+ x="322"

147+ y="468.36221"

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>

149+ <text

150+ sodipodi:linespacing="125%"

151+ id="text4160"

152+ y="325.36221"

153+ x="224"

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"

155+ xml:space="preserve"

156+ inkscape:export-xdpi="61.120499"

157+ 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"

159+ y="325.36221"

160+ x="224"

161+ id="tspan4162"

162+ sodipodi:role="line">fill (Var `{{x}})</tspan></text>

163+ <path

164+ sodipodi:nodetypes="cc"

165+ inkscape:connector-curvature="0"

166+ id="path4164"

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"

170+ inkscape:export-ydpi="61.120499" />

171+ <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)"

173+ d="m 273,330.3622 59,121"

174+ id="path5202"

175+ inkscape:connector-curvature="0"

176+ sodipodi:nodetypes="cc"

177+ inkscape:export-xdpi="61.120499"

178+ inkscape:export-ydpi="61.120499" />

179+ </g>

180+</svg>