tutorial/library.ltx · Idris-dev

git.iko.soy/Idris-dev

on d1663cc help sign in

Idris-dev/tutorial/library.ltx

325 lines 8.1 kB history raw

1%%%%%%%%%%%%%%% library file for datatypes etc.

3%%% Identifiers

5\newcommand{\va}{\VV{a}}

6\newcommand{\vb}{\VV{b}}

7\newcommand{\vc}{\VV{c}}

8\newcommand{\vd}{\VV{d}}

9\newcommand{\ve}{\VV{e}}

10\newcommand{\vf}{\VV{f}}

11\newcommand{\vg}{\VV{g}}

12\newcommand{\vh}{\VV{h}}

13\newcommand{\vi}{\VV{i}}

14\newcommand{\vj}{\VV{j}}

15\newcommand{\vk}{\VV{k}}

16\newcommand{\vl}{\VV{l}}

17\newcommand{\vm}{\VV{m}}

18\newcommand{\vn}{\VV{n}}

19\newcommand{\vo}{\VV{o}}

20\newcommand{\vp}{\VV{p}}

21\newcommand{\vq}{\VV{q}}

22\newcommand{\vr}{\VV{r}}

23\newcommand{\vs}{\VV{s}}

24\newcommand{\vt}{\VV{t}}

25\newcommand{\vu}{\VV{u}}

26\newcommand{\vv}{\VV{v}}

27\newcommand{\vw}{\VV{w}}

28\newcommand{\vx}{\VV{x}}

29\newcommand{\vy}{\VV{y}}

30\newcommand{\vz}{\VV{z}}

31\newcommand{\vA}{\VV{A}}

32\newcommand{\vB}{\VV{B}}

33\newcommand{\vC}{\VV{C}}

34\newcommand{\vD}{\VV{D}}

35\newcommand{\vE}{\VV{E}}

36\newcommand{\vF}{\VV{F}}

37\newcommand{\vG}{\VV{G}}

38\newcommand{\vH}{\VV{H}}

39\newcommand{\vI}{\VV{I}}

40\newcommand{\vJ}{\VV{J}}

41\newcommand{\vK}{\VV{K}}

42\newcommand{\vL}{\VV{L}}

43\newcommand{\vM}{\VV{M}}

44\newcommand{\vN}{\VV{N}}

45\newcommand{\vO}{\VV{O}}

46\newcommand{\vP}{\VV{P}}

47\newcommand{\vQ}{\VV{Q}}

48\newcommand{\vR}{\VV{R}}

49\newcommand{\vS}{\VV{S}}

50\newcommand{\vT}{\VV{T}}

51\newcommand{\vU}{\VV{U}}

52\newcommand{\vV}{\VV{V}}

53\newcommand{\vW}{\VV{W}}

54\newcommand{\vX}{\VV{X}}

55\newcommand{\vY}{\VV{Y}}

56\newcommand{\vZ}{\VV{Z}}

57\newcommand{\vas}{\VV{as}}

58\newcommand{\vbs}{\VV{bs}}

59\newcommand{\vcs}{\VV{cs}}

60\newcommand{\vds}{\VV{ds}}

61\newcommand{\ves}{\VV{es}}

62\newcommand{\vfs}{\VV{fs}}

63\newcommand{\vgs}{\VV{gs}}

64\newcommand{\vhs}{\VV{hs}}

65\newcommand{\vis}{\VV{is}}

66\newcommand{\vjs}{\VV{js}}

67\newcommand{\vks}{\VV{ks}}

68\newcommand{\vls}{\VV{ls}}

69\newcommand{\vms}{\VV{ms}}

70\newcommand{\vns}{\VV{ns}}

71\newcommand{\vos}{\VV{os}}

72\newcommand{\vps}{\VV{ps}}

73\newcommand{\vqs}{\VV{qs}}

74\newcommand{\vrs}{\VV{rs}}

75%\newcommand{\vss}{\VV{ss}}

76\newcommand{\vts}{\VV{ts}}

77\newcommand{\vus}{\VV{us}}

78\newcommand{\vvs}{\VV{vs}}

79\newcommand{\vws}{\VV{ws}}

80\newcommand{\vxs}{\VV{xs}}

81\newcommand{\vys}{\VV{ys}}

82\newcommand{\vzs}{\VV{zs}}

84%%% Telescope Identifiers

86\newcommand{\ta}{\vec{\VV{a}}}

87\newcommand{\tb}{\vec{\VV{b}}}

88\newcommand{\tc}{\vec{\VV{c}}}

89\newcommand{\td}{\vec{\VV{d}}}

90\newcommand{\te}{\vec{\VV{e}}}

91\newcommand{\tf}{\vec{\VV{f}}}

92\newcommand{\tg}{\vec{\VV{g}}}

93%\newcommand{\th}{\vec{\VV{h}}}

94\newcommand{\ti}{\vec{\VV{i}}}

95\newcommand{\tj}{\vec{\VV{j}}}

96\newcommand{\tk}{\vec{\VV{k}}}

97\newcommand{\tl}{\vec{\VV{l}}}

98\newcommand{\tm}{\vec{\VV{m}}}

99\newcommand{\tn}{\vec{\VV{n}}}

100%\newcommand{\to}{\vec{\VV{o}}}

101\newcommand{\tp}{\vec{\VV{p}}}

102\newcommand{\tq}{\vec{\VV{q}}}

103\newcommand{\tr}{\vec{\VV{r}}}

104\newcommand{\tts}{\vec{\VV{s}}}

105\newcommand{\ttt}{\vec{\VV{t}}}

106\newcommand{\tu}{\vec{\VV{u}}}

107%\newcommand{\tv}{\vec{\VV{v}}}

108\newcommand{\tw}{\vec{\VV{w}}}

109\newcommand{\tx}{\vec{\VV{x}}}

110\newcommand{\ty}{\vec{\VV{y}}}

111\newcommand{\tz}{\vec{\VV{z}}}

112\newcommand{\tA}{\vec{\VV{A}}}

113\newcommand{\tB}{\vec{\VV{B}}}

114\newcommand{\tC}{\vec{\VV{C}}}

115\newcommand{\tD}{\vec{\VV{D}}}

116\newcommand{\tE}{\vec{\VV{E}}}

117\newcommand{\tF}{\vec{\VV{F}}}

118\newcommand{\tG}{\vec{\VV{G}}}

119\newcommand{\tH}{\vec{\VV{H}}}

120\newcommand{\tI}{\vec{\VV{I}}}

121\newcommand{\tJ}{\vec{\VV{J}}}

122\newcommand{\tK}{\vec{\VV{K}}}

123\newcommand{\tL}{\vec{\VV{L}}}

124\newcommand{\tM}{\vec{\VV{M}}}

125\newcommand{\tN}{\vec{\VV{N}}}

126\newcommand{\tO}{\vec{\VV{O}}}

127\newcommand{\tP}{\vec{\VV{P}}}

128\newcommand{\tQ}{\vec{\VV{Q}}}

129\newcommand{\tR}{\vec{\VV{R}}}

130\newcommand{\tS}{\vec{\VV{S}}}

131\newcommand{\tT}{\vec{\VV{T}}}

132\newcommand{\tU}{\vec{\VV{U}}}

133\newcommand{\tV}{\vec{\VV{V}}}

134\newcommand{\tW}{\vec{\VV{W}}}

135\newcommand{\tX}{\vec{\VV{X}}}

136\newcommand{\tY}{\vec{\VV{Y}}}

137\newcommand{\tZ}{\vec{\VV{Z}}}

141%%% Nat

143\newcommand{\NatPackage}{

144 \newcommand{\Nat}{\TC{\mathbb{N}}}

145 \newcommand{\Z}{\DC{0}}

146 \newcommand{\suc}{\DC{s}}

147 \newcommand{\NatDecl}{

148 \Data \hg

149 \Axiom{\Nat\Hab\Type} \hg

150 \Where \hg

151 \Axiom{\Z\Hab\Nat} \hg

152 \Rule{\vn\Hab\Nat}

153 {\suc\:\vn\Hab\Nat}

154}}

155

156%%% Bool

157

158\newcommand{\BoolPackage}{

159 \newcommand{\Bool}{\TC{Bool}}

160 \newcommand{\true}{\DC{true}}

161 \newcommand{\false}{\DC{false}}

162 \newcommand{\BoolDecl}{

163 \Data \hg

164 \Axiom{\Bool\Hab\Type} \hg

165 \Where \hg

166 \Axiom{\true\Hab\Bool} \hg

167 \Axiom{\false\Hab\Bool}

168}}

169

170%%% So

171

172\newcommand{\SoPackage}{

173 \newcommand{\So}{\TC{So}}

174 \newcommand{\oh}{\DC{oh}}

175 \newcommand{\SoDecl}{

176 \Data \hg

177 \Rule{\vb\Hab\Bool}

178 {\So\:\vb\Hab\Type} \hg

179 \Where \hg

180 \Axiom{\oh\Hab\So\:\true}

181}}

182

183%%% Unit

184

185\newcommand{\UnitPackage}{

186 \newcommand{\Unit}{\TC{Unit}}

187 \newcommand{\void}{\DC{void}}

188 \newcommand{\UnitDecl}{

189 \Data \hg

190 \Axiom{\Unit\Hab\Type} \hg

191 \Where \hg

192 \Axiom{\void\Hab\Unit}

193}}

194

195%%% Maybe

196

197\newcommand{\MaybePackage}{

198 \newcommand{\Maybe}{\TC{Maybe}}

199 \newcommand{\yes}{\DC{yes}}

200 \newcommand{\no}{\DC{no}}

201 \newcommand{\MaybeDecl}{

202 \Data \hg

203 \Rule{\vA\Hab\Type}

204 {\Maybe\:\vA\Hab\Type} \hg

205 \Where \hg

206 \Rule{\va \Hab \vA}

207 {\yes\:\va\Hab\Maybe\:\vA} \hg

208 \Axiom{\no\Hab\Maybe\:\vA}

209}}

210

211%%% Cross

212

213\newcommand{\pr}[2]{(#1\DC{,}#2)} %grrrr

214\newcommand{\CrossPackage}{

215 \newcommand{\Cross}{\times}

216 \newcommand{\CrossDecl}{

217 \Data \hg

218 \Rule{\vA,\vB\Hab\Type}

219 {\vA\Cross\vB\Hab\Type} \hg

220 \Where \hg

221 \Rule{\va \Hab \vA \hg \vb\Hab\vB}

222 {\pr{\va}{\vb}\Hab\vA\Cross\vB}

223}}

224

225%%% Fin

226

227\newcommand{\FinPackage}{

228 \newcommand{\Fin}{\TC{Fin}}

229 \newcommand{\fz}{\DC{f0}}

230 \newcommand{\fs}{\DC{fs}}

231 \newcommand{\FinDecl}{

232 \AR{

233 \Data \hg

234 \Rule{\vn\Hab\Nat}

235 {\Fin\:\vn\Hab\Type} \hg \\

236 \Where \hg

237 \begin{array}[t]{c}

238 \Axiom{\fz\Hab\Fin\:(\suc\:\vn)} \hg

239 \Rule{\vi\Hab\Fin\:\vn}

240 {\fs\:\vi\Hab\Fin\:(\suc\:\vn)}

241 \end{array}

242 }

243}}

244

245%%% Vect

246

247\newcommand{\VectPackage}{

248 \newcommand{\Vect}{\TC{Vect}}

249 \newcommand{\vnil}{\varepsilon}

250 \newcommand{\vcons}{\,\dcolon\,}

251 \newcommand{\vsnoc}{\,\dcolon\,}

252 \newcommand{\VectConsDecl}{

253 \Data \hg

254 \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}

255 {\Vect\:\vA\:\vn\Hab\Type} \hg

256 \Where \hg \begin{array}[t]{c}

257 \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\

258 \Rule{\vx\Hab\vA \hg \vxs\Hab \Vect\:\vA\:\vn }

259 {\vx\vcons\vxs\Hab\Vect\:\vA\:(\suc\vn)}

260 \end{array}

261}

262 \newcommand{\VectSnocDecl}{

263 \Data \hg

264 \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}

265 {\Vect\:\vA\:\vn\Hab\Type} \hg

266 \Where \hg \begin{array}[t]{c}

267 \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\

268 \Rule{\vxs\Hab \Vect\:\vA\:\vn \hg \vx\Hab\vA}

269 {\vxs\vsnoc\vx\Hab\Vect\:\vA\:(\suc\vn)}

270 \end{array}

271}

272}

273

274%%% Compare

275

276%Data Compare : (x:nat)(y:nat)Type

277% = lt : (x:nat)(y:nat)(Compare x (plus (S y) x))

278% | eq : (x:nat)(Compare x x)

279% | gt : (x:nat)(y:nat)(Compare (plus (S x) y) y);

280

281

282\newcommand{\ComparePackage}{

283 \newcommand{\Compare}{\TC{Compare}}

284 \newcommand{\ltComp}{\DC{lt}}

285 \newcommand{\eqComp}{\DC{eq}}

286 \newcommand{\gtComp}{\DC{gt}}

287 \newcommand{\CompareDecl}{

288 \Data \hg

289 \Rule{\vm\Hab\Nat\hg\vn\Hab\Nat}

290 {\Compare\:\vm\:\vn\Hab\Type} \\

291 \Where \hg\begin{array}[t]{c}

292 \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}

293 {\ltComp_{\vx}\:\vy\Hab\Compare\:\vx\:(\FN{plus}\:\vx\:(\suc\:\vy))} \\

294 \Rule{\vx\Hab\Nat}

295 {\eqComp_{\vx}\Hab\Compare\:\vx\:\vx}\\

296 \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}

297 {\gtComp_{\vy}\:\vx\Hab\Compare\:(\FN{plus}\:\vy\:(\suc\:\vx))\:\vy} \\

298 \end{array}

299 }

300

301%Data CompareM : Type

302% = ltM : (ydiff:nat)CompareM

303% | eqM : CompareM

304% | gtM : (xdiff:nat)CompareM;

305

306 \newcommand{\CompareM}{\TC{Compare^-}}

307 \newcommand{\ltCompM}{\DC{lt^-}}

308 \newcommand{\eqCompM}{\DC{eq^-}}

309 \newcommand{\gtCompM}{\DC{gt^-}}

310 \newcommand{\CompareMDecl}{

311

312 \Data \hg

313 \Axiom{\CompareM\Hab\Type} \\

314 \Where \hg\begin{array}[t]{c}

315 \Rule{\vy\Hab\Nat}

316 {\ltCompM\:\vy\Hab\CompareM} \\

317 \Axiom{\eqCompM\Hab\CompareM}\\

318 \Rule{\vx\Hab\Nat}

319 {\gtCompM\:\vx\Hab\CompareM} \\

320 \end{array}

321 }

322 \newcommand{\CompareRec}{\FN{CompareRec}}

323 \newcommand{\CompareRecM}{\FN{CompareRec^-}}

324

325}