tutorial/macros.ltx · Idris-dev

git.iko.soy/Idris-dev

on ef93607 help sign in

Idris-dev/tutorial/macros.ltx

1066 lines 32 kB history raw

1%\usepackage{amstex}

2\usepackage{amssymb}

3\usepackage{latexsym}

4\usepackage{eepic}

7%%%%%%%%% INFERENCE RULES

9\newlength{\rulevgap}

10\setlength{\rulevgap}{0.05in}

11\newlength{\ruleheight}

12\newlength{\ruledepth}

13\newsavebox{\rulebox}

14\newlength{\GapLength}

15\newcommand{\gap}[1]{\settowidth{\GapLength}{#1} \hspace*{\GapLength}}

16\newcommand{\dotstep}[2]{\begin{tabular}[b]{@{}c@{}}

17 #1\\$\vdots$\\#2

18 \end{tabular}}

19\newlength{\fracwid}

20\newcommand{\dotfrac}[2]{\settowidth{\fracwid}{$\frac{#1}{#2}$}

21 \addtolength{\fracwid}{0.1in}

22 \begin{tabular}[b]{@{}c@{}}

23 $#1$\\

24 \parbox[c][0.02in][t]{\fracwid}{\dotfill} \\

25 $#2$\\

26 \end{tabular}}

27\newcommand{\Rule}[2]{\savebox{\rulebox}[\width][b] %

28 {$ \frac{\raisebox{0in} {\( #1 $}} %

29 {\raisebox{-0.03in}{$ #2 $}} \)} %

30 \settoheight{\ruleheight}{\usebox{\rulebox}} %

31 \addtolength{\ruleheight}{\rulevgap} %

32 \settodepth{\ruledepth}{\usebox{\rulebox}} %

33 \addtolength{\ruledepth}{\rulevgap} %

34 \raisebox{0in}[\ruleheight][\ruledepth] %

35 {\usebox{\rulebox}}}

36\newcommand{\Case}[2]{\savebox{\rulebox}[\width][b] %

37 {$ \dotfrac{\raisebox{0in} {\( #1 $}} %

38 {\raisebox{-0.03in}{$ #2 $}} \)} %

39 \settoheight{\ruleheight}{\usebox{\rulebox}} %

40 \addtolength{\ruleheight}{\rulevgap} %

41 \settodepth{\ruledepth}{\usebox{\rulebox}} %

42 \addtolength{\ruledepth}{\rulevgap} %

43 \raisebox{0in}[\ruleheight][\ruledepth] %

44 {\usebox{\rulebox}}}

45\newcommand{\Axiom}[1]{\savebox{\rulebox}[\width][b] %

46 {$\frac{}{\raisebox{-0.03in}{$#1$}}$} %

47 \settoheight{\ruleheight}{\usebox{\rulebox}} %

48 \addtolength{\ruleheight}{\rulevgap} %

49 \settodepth{\ruledepth}{\usebox{\rulebox}} %

50 \addtolength{\ruledepth}{\rulevgap} %

51 \raisebox{0in}[\ruleheight][\ruledepth] %

52 {\usebox{\rulebox}}}

53\newcommand{\RuleSide}[3]{\gap{$#2$} \hspace*{0.1in} %

54 \Rule{#1}{#3} %

55 \hspace*{0.1in}$#2$}

56\newcommand{\AxiomSide}[2]{\gap{$#1$} \hspace*{0.1in} %

57 \Axiom{#2} %

58 \hspace*{0.1in}$#1$}

59\newcommand{\RULE}[1]{\textbf{#1}}

60\newcommand{\hg}{\hspace{0.2in}}

62\newcommand{\ProofState}

63 [2]{\parbox{10cm}{\AR{\hg\AR{#1}\\\Axiom{\hg#2\hg}}}}

65%%%%%%%%%%%% TRISTUFF

67\newcommand{\btr}{

68\setlength{\unitlength}{0.0005in}

69\begin{picture}(69,180)(0,12)

70\blacken\path(57,192)(57,12)(12,102)

71 (57,192)(57,192)

72\path(57,192)(57,12)(12,102)

73 (57,192)(57,192)

74\end{picture}

75}

77\newcommand{\btl}{

78\setlength{\unitlength}{0.0005in}

79\begin{picture}(69,180)(0,12)

80\blacken\path(12,192)(12,12)(57,102)

81 (12,192)(12,192)

82\path(12,192)(12,12)(57,102)

83 (12,192)(12,192)

84\end{picture}

85}

87\newcommand{\wtr}{

88\setlength{\unitlength}{0.0005in}

89\begin{picture}(69,180)(0,12)

90%\blacken\path(57,192)(57,12)(12,102)

91% (57,192)(57,192)

92\path(57,192)(57,12)(12,102)

93 (57,192)(57,192)

94\end{picture}

95}

97\newcommand{\wtl}{

98\setlength{\unitlength}{0.0005in}

99\begin{picture}(69,180)(0,12)

100%\blacken\path(12,192)(12,12)(57,102)

101% (12,192)(12,192)

102\path(12,192)(12,12)(57,102)

103 (12,192)(12,192)

104\end{picture}

105}

106

107

108

109%%%%%%%%%%%% FONTS

110

111\newcommand{\TC}[1]{\mathsf{#1}}

112\newcommand{\DC}[1]{\mathsf{#1}}

113\newcommand{\VV}[1]{\mathit{#1}}

114\newcommand{\FN}[1]{\mathbf{#1}}

115\newcommand{\HFN}[1]{\mathtt{#1}}

116\newcommand{\RW}[1]{\underline{\textrm{#1}}}

117\newcommand{\MO}[1]{\mbox{\textsc{#1}}}

118

119\newcommand{\tTC}[1]{\texttt{#1}}

120\newcommand{\tDC}[1]{\texttt{#1}}

121\newcommand{\tFN}[1]{\texttt{#1}}

122

123\newcommand{\HF}[1]{\mathtt{#1}}

124

125\newcommand{\MV}[1]{\nhole\mathit{#1}}

126\newcommand{\Lang}[1]{\mathsf{#1}}

127\newcommand{\Name}[1]{\mathit{#1}}

128

129\newcommand{\demph}[1]{\textbf{#1}}

130\newcommand{\remph}[1]{\emph{#1}}

131

132%%%% Keywords for meta operations

133\newcommand{\IF}{\;\RW{if}\;\;}

134\newcommand{\THEN}{\RW{then}}

135\newcommand{\ELSE}{\RW{else}}

136\newcommand{\AND}{\RW{and}}

137\newcommand{\Otherwise}{\RW{otherwise}}

138\newcommand{\Do}{\RW{do}}

139\newcommand{\Return}{\RW{return}}

140

141\newcommand{\CASE}{\RW{case}}

142\newcommand{\LET}{\RW{let}}

143\newcommand{\IN}{\RW{in}}

144\newcommand{\of}{\RW{of}}

145

146\newcommand{\CLASS}{\mathtt{class}}

147\newcommand{\INSTANCE}{\mathtt{instance}}

148

149%%%%%%%%%%%% GROUPING

150

151\newcommand{\G}{

152\setlength{\unitlength}{1pt}

153\begin{picture}(4,10)(0,0)

154\path(2,10)(2,-10)

155\end{picture}

156}

157

158\newcommand{\E}{

159\setlength{\unitlength}{1pt}

160\begin{picture}(4,10)(0,0)

161\path(2,10)(2,-2)(4,-2)

162\end{picture}

163}

164

165%\newcommand{\C}{

166%\setlength{\unitlength}{1pt}

167%\begin{picture}(4,10)(0,0)

168%\path(4,8)(2,8)(2,-2)(4,-2)

169%\end{picture}

170%}

171

172\newcommand{\M}{

173\setlength{\unitlength}{1pt}

174\begin{picture}(4,10)(0,0)

175\path(2,10)(2,-2)(6,-2)

176\end{picture}

177}

178

179\newcommand{\F}{

180\setlength{\unitlength}{1pt}

181\begin{picture}(4,10)(0,0)

182\path(4,8)(2,8)(2,-6)

183\end{picture}

184}

185

186\newcommand{\K}{

187\setlength{\unitlength}{1pt}

188\begin{picture}(4,10)(0,0)

189\path(0,8)(4,8)

190\end{picture}

191}

192

193\newcommand{\J}{

194\setlength{\unitlength}{1pt}

195\begin{picture}(4,10)(0,0)

196\path(0,-2)(4,-2)

197\end{picture}

198}

199

200\newcommand{\W}{

201\setlength{\unitlength}{1pt}

202\begin{picture}(4,10)(0,0)

203\end{picture}

204}

205

206

207

208%%%%%%%%%%%% GUBBINS

209

210\newcommand{\mathskip}{\medskip}

211

212\newcommand{\fbx}[1]{\fbox{$#1$}}

213\newcommand{\stk}[1]{\begin{array}{c}#1\end{array}}

214%\newcommand{\DM}[1]{\hg\mbox{$#1$}}

215\newcommand{\DM}[1]{\mathskip\par$#1$\mathskip}

216\newcommand{\mbx}[1]{\mathskip\par\noindent$#1$\mathskip}

217\newcommand{\AR}[1]{\begin{array}[t]{@{}l}#1\end{array}}

218\newcommand{\ARt}[1]{\begin{array}[t]{@{}l@{}cl}#1\end{array}}

219\newcommand{\ARc}[1]{\begin{array}{@{}l}#1\end{array}}

220\newcommand{\ARd}[1]{\begin{array}[t]{cl}#1\end{array}}

221\newcommand{\DAR}[1]{\begin{array}{ll}\hg & #1\end{array}}

222\newcommand{\Dor}{\\ \hg\mid & }

223\newcommand{\EA}[1]{\begin{array}[t]{r@{}c@{}l}#1\end{array}}

224\newcommand{\A}{@{\:}c}

225%\newcommand{\R}{@{\:}r}

226\newcommand{\CA}{c}

227\newcommand{\LA}{l}

228\newcommand{\PAc}[2]{\begin{array}{l#1@{}r@{}l}#2\end{array}}

229\newcommand{\PA}[2]{\begin{array}[t]{l@{\:}l#1@{}r@{\:}l}#2\end{array}}

230\newcommand{\DTREE}[3]{\begin{array}[t]{l#1@{}r@{\:}l#2}#3\end{array}}

231\newcommand{\IDTREE}[2]{%

232 \begin{array}[t]{l@{\:}c@{\:}l@{\:}r@{\:}l#1}#2\end{array}}

233\newcommand{\IA}[2]

234 {\begin{array}[t]{l@{\:}r@{\:}c@{\:}l@{\:}#1@{\:}r@{\:}l}#2\end{array}}

235\newcommand{\IAc}[2]

236 {\begin{array}[c]{r@{\:}c@{\:}l@{\:}#1@{}r@{}l}#2\end{array}}

237\newcommand{\CS}[1]{\left\lfloor\begin{array}{@{}l}#1\end{array}\right.}

238\newcommand{\BY}[3]{\multicolumn{2}{l}{\;\RW{by}\; #1} \\ %

239 \multicolumn{#2}{l}{\CS{#3}} }

240\newcommand{\WITH}[3]{\multicolumn{2}{l}{\;\RW{with}\; #1} \\ %

241 \multicolumn{#2}{l}{\CS{#3}} }

242\newcommand{\WithBy}{\RW{with-by}}

243\newcommand{\Wb}[1]{\WithBy& #1}

244\newcommand{\By}[1]{\multicolumn{2}{l}{\Leftarrow #1}}

245\newcommand{\andby}{\Leftarrow}

246\newcommand{\MyWith}[1]{\multicolumn{2}{l}{|\;#1}}

247\newcommand{\Byr}[1]{\;\RW{by}\; #1}

248

249\newcommand{\Bar}{|}

250\newcommand{\Bart}{\settowidth{\GapLength}{$\Bar$}%

251 \raisebox{6pt}[0pt][0pt]{$\Bar$}%

252 \hspace*{-1\GapLength}%

253 \Bar}

254\newcommand{\With}[1]{\Bar & #1}

255\newcommand{\Witt}[1]{\Bart & #1}

256

257\newcommand{\B}{@{\:}r@{\:}c}

258\newcommand{\Ret}[1]{\multicolumn{2}{l}{\cq #1}}

259\newcommand{\MRet}[2]{\multicolumn{#1}{l}{\cq #2}}

260\newcommand{\HRet}[1]{\multicolumn{2}{l}{\hq #1}}

261\newcommand{\MHRet}[2]{\multicolumn{#1}{l}{\hq #2}}

262\newcommand{\IRet}[1]{\multicolumn{2}{l}{\iq #1}}

263\newcommand{\IMRet}[2]{\multicolumn{#1}{l}{\iq #2}}

264\newcommand{\MoRet}[1]{\multicolumn{2}{l}{\mq #1}}

265\newcommand{\MMoRet}[2]{\multicolumn{#1}{l}{\mq #2}}

266\newcommand{\Data}{\RW{data}}

267\newcommand{\Codata}{\RW{codata}}

268\newcommand{\Where}{\RW{where}}

269\newcommand{\Let}{\RW{let}}

270\newcommand{\Fact}{\RW{fact}}

271\newcommand{\Rec}[1]{#1\textbf{-Rec}}

272\newcommand{\Memo}[1]{#1\textbf{-Memo}}

273\newcommand{\Elim}[1]{#1\textbf{-Elim}}

274\newcommand{\Cases}[1]{#1\textbf{-Case}}

275\newcommand{\View}[1]{#1\textbf{-View}}

276\newcommand{\As}[2]{#1 \:\RW{as}\: #2}

277\newcommand{\nhole}{\Box}

278\newcommand{\turq}{\:\vdash_?\:}

279\newcommand{\split}{\;\lhd\;}

280\newcommand{\CType}[2]{\{#1 \split\; #2\}}

281\newcommand{\CC}[2]{(#1)\:#2}

282\newcommand{\UP}[2]{#1 | \{#2\}}

283\newcommand{\Ured}{\:\Downarrow\:}

284\newcommand{\gdd}{\prec}

285\newcommand{\HC}[1]{\left<#1\right>}

286\newcommand{\HT}[2]{\left<#1 \hab #2\right>}

287

288\newcommand{\view}{\RW{view}}

289\newcommand{\ecase}{\RW{case}}

290\newcommand{\rec}{\RW{rec}}

291

292\newcommand{\If}{\mathsf{if}}

293\newcommand{\Then}{\mathsf{then}}

294\newcommand{\Else}{\mathsf{else}}

295\newcommand{\elim}{\RW{elim}}

296

297\newcommand{\Payload}{\mathsf{type}}

298\newcommand{\Any}{\mathsf{Some}}

299

300\newcommand{\lbl}[2]{\langle #1 \Hab #2 \rangle}

301\newcommand{\call}[2]{\RW{call}\:\langle#1\rangle\:#2}

302\newcommand{\return}[1]{\RW{return}\:#1}

303

304\newcommand{\Remark}[1]{\noindent\textbf{Remark:} #1}

305

306\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}

307

308\newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}

309\newcommand{\useverb}[1]{\BUseVerbatim{#1}}

310\newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

311\newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}

312

313\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}

314\caption{#3}\label{#2}\end{figure}}

315\newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

316\newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}

317\newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

318\newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

319\newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}

320\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}

321\caption{#3}\label{#2}\end{figure*}}

322

323\newcommand{\FIG}[3]{\begin{figure}[h]\DM{#1}\caption{#2}\label{#3}\end{figure}}

324\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

325\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

326\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}

327\newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}

328\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}

329\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

330

331\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}

332\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}

333

334\newcommand{\RESFIG}[3]{

335\TFIG{|l|c|c|c|c|c|c|c|c|}{

336\hline

337 & \multicolumn{4}{c|}{\Naive{} compilation} &

338 \multicolumn{4}{|c|}{Optimised compilation} \\

339\cline{2-9}

340\raisebox{1.5ex}[0pt]{Program} & Instrs & Thunks & Cells &

341Accesses & Instructions & Thunks & Cells & Accesses \\

342%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\

343\hline

344#1

345\hline

346}{#2}{#3}}

347

348\newcommand{\NEWRESFIG}[3]{

349\TFIG{|l|l|c|c|c|c|}{

350\hline

351% & \multicolumn{4}{c|}{\Naive{} compilation} &

352% \multicolumn{4}{|c|}{Optimised compilation} \\

353%\cline{2-9}

354Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

355%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\

356\hline

357#1

358}{#2}{#3}}

359

360\newcommand{\NEWRESFIGTC}[3]{

361\TFIGTC{|l|l|c|c|c|c|}{

362\hline

363% & \multicolumn{4}{c|}{\Naive{} compilation} &

364% \multicolumn{4}{|c|}{Optimised compilation} \\

365%\cline{2-9}

366Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

367%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\

368\hline

369#1

370}{#2}{#3}}

371

372\newcommand{\RESLINE}[9]{

373& \Naive{} & #2 & #3 & #5 & #4 \\

374#1

375& Optimised & #6 & #7 & #9 & #8 \\

376}

377\newcommand{\RESCHANGE}[4]{

378& Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\

379\hline

380}

381\newcommand{\RESCHANGEa}[5]{

382#5 & Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\

383\hline

384}

385

386%%%%%%%%%%%% PUNCTUATION

387

388\newcommand{\pad}[2]{#1#2#1}

389

390\newcommand{\hab}{\pad{\,}{:}}

391\newcommand{\Hab}{\pad{\;}{:}}

392\newcommand{\HHab}{\pad{\;}{::}}

393

394%%%%%%%%%%%% TYPE

395

396\newcommand{\Type}{\mbox{\texttt{\#}}} %\star}

397

398

399%%%%%%%%%%%%% ARROWS

400

401\newcommand{\To}{\pad{\:}{\rightarrow}}

402\newcommand{\Gets}{\leftarrow}

403%\newcommand{\car}{\vartriangleright}

404

405%%%%%%%%%%%%% QUANTIFIERS

406

407\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}

408\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}

409\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}

410\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}

411\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}

412\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}

413\newcommand{\remall}[2]{\forall\{#1\pad{\!}{:}#2\}}

414\newcommand{\allpi}[2]{\Pi#1\pad{\!}{:}#2}

415\newcommand{\ali}[2]{\forall#1|#2}

416\newcommand{\exi}[2]{\exists#1\pad{\!}{:}#2}

417\newcommand{\wit}[2]{\ang{#1,#2}}

418\newcommand{\X}{\times}

419\newcommand{\sig}[2]{\Sigma#1\pad{\!}{:}#2}

420

421\newcommand{\SC}{.\:}

422

423\newcommand{\letbind}[3]{\mathsf{let}\:#1{:}#2\:=\:#3\:\mathsf{in}}

424\newcommand{\ifthen}[3]{\mathsf{if}\:#1\:\mathsf{then}\:#2\:\mathsf{else}\:#3}

425

426%%%%%%%%%%%%% EQUALITIES

427

428\newcommand{\cq}{\pad{\:}{\mapsto}}

429\newcommand{\xq}{\pad{}{\doteq}}

430\newcommand{\pq}{\pad{\:}{=}}

431\newcommand{\dq}{\pad{\:}{:=}}

432\newcommand{\iq}{\pad{\:}{\leadsto}}

433\newcommand{\mq}{\Longrightarrow}

434\newcommand{\retq}{\Rightarrow}

435\newcommand{\hq}{\pad{\:}{=}}

436\newcommand{\defq}{\mapsto}

437

438\newcommand{\refl}{\TC{refl}}

443%%%%%%%%%%%%% CATSTUFF

444

445\newlength{\Lwibrs}

446\newlength{\Lwobrs}

447\newsavebox{\Bwibrs}

448\newsavebox{\Bwobrs}

449\newcommand{\Db}[5]{%

450 \savebox{\Bwobrs}[\width][b]{$#5$}%

451 \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right#3$}%

452 \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%

453 \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%

454 \addtolength{\Lwibrs}{-\Lwobrs}%

455 \left#1\pad{\hspace*{-0.25\Lwibrs}}{\usebox{\Bwibrs}}\right#4}

456\newcommand{\LDb}[3]{%

457 \savebox{\Bwobrs}[\width][b]{$#3$}%

458 \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right.$}%

459 \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%

460 \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%

461 \addtolength{\Lwibrs}{-\Lwobrs}%

462 \left#1\hspace*{-0.4\Lwibrs}\usebox{\Bwibrs}\right.}

463\newcommand{\RDb}[3]{%

464 \savebox{\Bwobrs}[\width][b]{$#3$}%

465 \savebox{\Bwibrs}[\width][b]{$\left.\usebox{\Bwobrs}\right#1$}%

466 \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%

467 \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%

468 \addtolength{\Lwibrs}{-\Lwobrs}%

469 \left.\usebox{\Bwibrs}\hspace*{-0.4\Lwibrs}\right#2}

470\newcommand{\Sc}{\Db{[}{[}{]}{]}}

471\newcommand{\Mo}{\Db{|}{>}{<}{|}}

472\newcommand{\MoL}{\LDb{|}{>}}

473\newcommand{\MoR}{\RDb{<}{|}}

474

475\newcommand{\car}{\mbox{$-\!\triangleright$}}

476\newcommand{\io}[1]{\iota_{#1}}

477\newcommand{\cc}{\diamond}

478

479

480%%%%%%%%%%%%% FNS

481

482\newcommand{\Wk}{\Uparrow}

483

484%%%%%%%%%%%%% Transformation

485

486\newcommand{\Transform}[3]{\textsc{Trans}\:_{\Name{#1}}

487 \interp{#2}\:\mq\:#3}

488%\:[\:#2\:\Longrightarrow\:#3\:]}

489\newcommand{\Morphism}[2]{\textsc{Morphism}\:#1\:\Longrightarrow\:#2}

490\newcommand{\MI}[1]{\begin{array}{ll} #1 \end{array}\\}

491\newcommand{\MorphItem}[2]{& #1 \:\Longrightarrow\: #2}

492

493%%%%%%%%%%%%% Stuff

494

495% Motive and methods

496

497\newcommand{\motive}{\vP}

498\newcommand{\meth}[1]{\vm_{#1}}

499

500% Tuples

501\newcommand{\tuple}[1]{\langle#1\rangle}

502\newcommand{\Tuple}[1]{\mathsf{Tuple}}

503\newcommand{\proj}{\mathsf{proj}}

504\newcommand{\app}{\mathrm{+\!+}}

505

506% Commenting out

507\newcommand{\ig}[1]{[#1]}

508\newcommand{\rem}[1]{\{\!#1\!\}}

509\newcommand{\igc}[1]{[#1]}

510\newcommand{\remc}[1]{\{\!#1\!\}}

511

512

513\newcommand{\ind}{\hspace*{0.1cm}}

514

515% Content free type

516\newcommand{\CF}{\TC{CF}}

517\newcommand{\cf}{\DC{cf}}

518

519% Error token

520\newcommand{\error}{\DC{error}}

521\newcommand{\fail}{\perp}

522

523% Constructor stripping

524\newcommand{\conarg}[2]{#1!#2}

525

526\newcommand{\Vect}{\TC{Vect}}

527\newcommand{\VectM}{\TC{Vect^-}}

528\newcommand{\Vnil}{\DC{\epsilon}}

529\newcommand{\Vcons}{\DC{::}}

530

531\newcommand{\Vsnoc}{\DC{::}}

532

533\newcommand{\VnilM}{\DC{\epsilon^-}}

534\newcommand{\VconsM}{\DC{::^-}}

535

536\newcommand{\Vnilcase}{\VV{vNilCase}}

537\newcommand{\Vconscase}{\VV{vConsCase}}

538

539\newcommand{\DSigma}{\TC{Sigma}}

540\newcommand{\Exists}{\DC{Exists}}

541

542\newcommand{\ListPair}[2]{\sig{#1}{\List\:\vA}.#2 = \FN{length}\:#1}

543\newcommand{\lpNilDef}{\lpNil{\FN{refl}\:\Z}}

544\newcommand{\lpNil}[1]{(\nil\:\vA,#1)}

545\newcommand{\lpConsDef}[3]{\lpCons{#1}{(\FN{fst\:#2})}{\FN{resp}\:(\FN{snd}\:#2)}}

546\newcommand{\lpCons}[3]{(\cons\:#1\:#2,#3)}

547\newcommand{\lp}[2]{(#1, #2)}

548

549\newcommand{\VnilTop}{\DC{vNil}^\ast}

550\newcommand{\VconsTop}{\DC{vCons}^\ast}

551

552\newcommand{\VnilBot}{\DC{\epsilon}^-}

553\newcommand{\VconsBot}{\DC{::}^-}

554

555\newcommand{\VectTop}{\TC{Vect}^\ast}

556\newcommand{\VectBot}{\TC{Vect}^-}

557

558\newcommand{\VectDrop}{\FN{vectDropIdx}}

559\newcommand{\VectRebuild}{\FN{vectRebuild}}

560

561\newcommand{\Prop}{\TC{Prop}}

562\newcommand{\Set}{\TC{Set}}

563\newcommand{\CoqType}{\TC{Type}}

564

565\newcommand{\List}{\TC{List}}

566\newcommand{\nil}{\DC{nil}}

567\newcommand{\cons}{\DC{cons}}

568

569\newcommand{\Zip}{\TC{Tsil}}

570\newcommand{\zip}{\FN{tsil}}

571\newcommand{\zipcons}{\FN{tsilcons}}

572\newcommand{\snoc}{\DC{Snoc}}

573\newcommand{\lin}{\DC{Empty}}

574

575\newcommand{\BigInt}{\TC{BigInt}}

576\newcommand{\False}{\TC{False}}

577\newcommand{\Unit}{\TC{Unit}}

578\newcommand{\UnitI}{\DC{unit}}

579

580\newcommand{\genType}{\TC{X}}

581\newcommand{\genIndicesDec}{\tb\Hab\tB}

582\newcommand{\genIndices}{\tb}

583\newcommand{\genConArgsDec}[1]{\vec{\VV{a_#1}}\Hab\vec{\VV{A_#1}}}

584\newcommand{\genConArgs}[1]{\vec{\VV{a_#1}}}

585\newcommand{\genConIndicesDec}[1]{\vec{\VV{b_#1}}\Hab\vec{\VV{B_#1}}}

586\newcommand{\genConIndices}[1]{\vec{\VV{b_#1}}}

587\newcommand{\genCon}[1]{\DC{x}_#1}

588

589\newcommand{\genTypeTop}{\TC{X^\ast}}

590\newcommand{\genTypeBot}{\TC{X^-}}

591

592\newcommand{\genTypeDrop}{\FN{XDropIdx}}

593\newcommand{\genTypeRebuild}{\FN{XRebuild}}

594

595\newcommand{\HTerm}{\texttt{Term}}

596\newcommand{\Term}{\TC{Term}}

597\newcommand{\Var}{\DC{var}}

598\newcommand{\Lam}{\DC{lam}}

599\newcommand{\App}{\DC{app}}

600\newcommand{\TermM}{\TC{Term^-}}

601\newcommand{\VarM}{\DC{var^-}}

602\newcommand{\LamM}{\DC{lam^-}}

603\newcommand{\AppM}{\DC{app^-}}

604\newcommand{\Env}{\TC{Env}}

605\newcommand{\SType}{\TC{STy}}

606\newcommand{\farrow}{\Rightarrow}

607\newcommand{\lookup}{\FN{lookup}}

608

609% \newcommand{\source}{\Lang{TT}}

610\newcommand{\source}{\textbf{DT-Res}}

611\newcommand{\target}{\Lang{ExTT}}

612\newcommand{\runtime}{\Lang{RunTT}}

613

614\newcommand{\lt}{\TC{<}}

615\newcommand{\ltO}{\DC{ltO}}

616\newcommand{\ltS}{\DC{ltS}}

617

618\newcommand{\interp}[1]{\llbracket #1 \rrbracket}

619\newcommand{\inferrable}[2]{\FN{inferrable}(#1,#2)}

620\newcommand{\mkPat}{\FN{mkPat}}

621

622\newcommand{\FinM}{\TC{Fin^-}}

623\newcommand{\fzM}{\DC{f0^-}}

624\newcommand{\fsM}{\DC{fs^-}}

625

626\newcommand{\concat}{\mathrm{++}}

627

628%\newcommand{\bottom}{\perp}

629

630% Reductions

631

632\newcommand{\reduces}{\mapsto}

633\newcommand{\translation}{\Rightarrow}

634%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}

635%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}

636\newcommand{\reducesn}[1]{\reduces_{#1}}

637\newcommand{\reducesto}{\reduces^{*}}

638

639% Equality

640

641\newcommand{\Refl}{\DC{refl}}

642\newcommand{\leZ}{\DC{O_{\le}}}

643\newcommand{\leS}{\DC{S_{\le}}}

644

645% Random elimination things

646

647\newcommand{\lte}{\TC{\leq}}

648\newcommand{\lten}{\DC{leN}}

649\newcommand{\lteO}{\DC{leO}}

650\newcommand{\lteS}{\DC{leS}}

651

652\newcommand{\ltelim}{\Elim{\lt}}

653\newcommand{\leelim}{\Elim{\lte}}

654

655\newcommand{\dD}{\TC{D}}

656\newcommand{\delim}{\Elim{\TC{D}}}

657\newcommand{\drec}{\Rec{\TC{D}}}

658\newcommand{\dcase}{\Cases{\TC{D}}}

659\newcommand{\dview}{\View{\TC{D}}}

660\newcommand{\dmemo}{\Memo{\TC{D}}}

661\newcommand{\natrec}{\Rec{\Nat}}

662\newcommand{\natmemo}{\Memo{\Nat}}

663\newcommand{\natmemogen}{\Nat\textbf{-MemoGen}}

664\newcommand{\natelim}{\Elim{\Nat}}

665\newcommand{\boolcase}{\Cases{\Bool}}

666\newcommand{\vectrec}{\Rec{\Vect}}

667\newcommand{\vectelim}{\Elim{\Vect}}

668\newcommand{\listrec}{\Rec{\List}}

669\newcommand{\listelim}{\Elim{\List}}

670\newcommand{\finrec}{\Rec{\Fin}}

671\newcommand{\finelim}{\Elim{\Fin}}

672\newcommand{\natcase}{\Cases{\Nat}}

673\newcommand{\vectcase}{\Cases{\Vect}}

674\newcommand{\natdoublerec}{\Nat\textbf{-double-elim}}

675\newcommand{\eqelim}{=\textbf{-elim}}

676\newcommand{\falsecase}{\Cases{\False}}

677

678% Code

679\newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}

680

681% Quicksort

682

683\newcommand{\QSView}{\TC{QuickSort}}

684\newcommand{\qsempty}{\DC{empty}}

685\newcommand{\partition}{\DC{partition}}

686\newcommand{\qsview}{\FN{mkQuickSort}}

687

688% More gubbins

689

690\newcommand{\converts}{\simeq}

691\newcommand{\cumul}{\preceq}

692\newcommand{\whnf}{\Downarrow}

693\newcommand{\elem}{\in}

694\newcommand{\proves}{\vdash}

695\newcommand{\biimplies}{\Longleftrightarrow}

696

697\newcommand{\lc}{\lambda_{\mathsf{AC}}}

698\newcommand{\zed}{\mathbb{Z}}

699

700% Haskell keywords

701

702\newcommand{\hdata}{\mathtt{data}}

703\newcommand{\newtype}{\mathtt{newtype}}

704%\newcommand{\htype}{\mathtt{type}}

705

706\newcommand{\HTC}[1]{\mathtt{#1}}

707\newcommand{\HDC}[1]{\mathtt{#1}}

708

709% Nobby

710

711\newcommand{\Value}{\HTC{Value}}

712\newcommand{\VGamma}{\HTC{Env}}

713\newcommand{\Ctxt}{\HTC{Ctxt}}

714\newcommand{\Defs}{\HTC{Defs}}

715\newcommand{\ECtxt}{\HTC{ECtxt}}

716\newcommand{\TCtxt}{\HTC{TCtxt}}

717\newcommand{\VG}{\HDC{Env}}

718\newcommand{\Model}{\HTC{Model}}

719\newcommand{\Const}{\HTC{Const}}

720\newcommand{\Normal}{\HTC{Normal}}

721\newcommand{\Scope}{\HTC{Scope}}

722\newcommand{\Kripke}{\HTC{Kripke}}

723\newcommand{\Weakening}{\HTC{Weakening}}

724\newcommand{\Ready}{\HTC{Ready}}

725\newcommand{\Blocked}{\HTC{Blocked}}

726\newcommand{\Spine}{\HTC{Spine}}

727

728\newcommand{\BV}{\HDC{BV}}

729\newcommand{\BCon}{\HDC{BCon}}

730\newcommand{\BTyCon}{\HDC{BTyCon}}

731\newcommand{\RCon}{\HDC{RCon}}

732\newcommand{\RTyCon}{\HDC{RTyCon}}

733\newcommand{\BElim}{\HDC{BElim}}

734\newcommand{\DV}{\HDC{V}}

735\newcommand{\DP}{\HDC{P}}

736

737\newcommand{\MR}{\HDC{R}}

738\newcommand{\MB}{\HDC{B}}

739\newcommand{\DSc}{\HDC{Sc}}

740\newcommand{\DKr}{\HDC{Kr}}

741\newcommand{\DWk}{\HDC{Wk}}

742\newcommand{\DSnoc}{\HDC{;}}

743\newcommand{\DType}{\HDC{Type}}

744\newcommand{\DName}{\HDC{Name}}

745\newcommand{\DInt}{\HDC{Int}}

746\newcommand{\DString}{\HDC{String}}

747\newcommand{\DElim}{\HDC{Elim}}

748\newcommand{\Empty}{\HDC{\emptyset}}

749

750\newcommand{\ConCode}{\HTC{ConCode}}

751\newcommand{\ElimRule}{\HTC{ElimRule}}

752

753\newcommand{\DConst}{\HDC{Const}}

754\newcommand{\DCon}{\HDC{Con}}

755\newcommand{\DTyCon}{\HDC{TyCon}}

756\newcommand{\RConst}{\HDC{RConst}}

757\newcommand{\RLam}{\HDC{RLam}}

758\newcommand{\RPi}{\HDC{RPi}}

759\newcommand{\DLam}{\HDC{Lam}}

760\newcommand{\DLet}{\HDC{Let}}

761\newcommand{\DPi}{\HDC{Pi}}

762\newcommand{\DApp}{\HDC{App}}

763

764\newcommand{\TMaybe}{\HTC{Maybe}}

765\newcommand{\DNothing}{\HDC{Nothing}}

766\newcommand{\DJust}{\HDC{Just}}

767

768

769% G-machine and heap

770

771\newcommand{\PUSH}{\mathsf{PUSH}}

772\newcommand{\PUSHNAME}{\mathsf{PUSHNAME}}

773\newcommand{\POP}{\mathsf{DISCARD}}

774\newcommand{\PUSHFUN}{\mathsf{PUSHFUN}}

775\newcommand{\APPLY}{\mathsf{MKAP}}

776\newcommand{\EVAL}{\mathsf{EVAL}}

777\newcommand{\GCON}{\mathsf{MKCON}}

778\newcommand{\GTUP}{\mathsf{MKTUP}}

779\newcommand{\GTYPE}{\mathsf{MKTYPE}}

780\newcommand{\UPDATE}{\mathsf{UPDATE}}

781\newcommand{\RET}{\mathsf{RET}}

782\newcommand{\UNWIND}{\mathsf{UNWIND}}

783\newcommand{\CASEJUMP}{\mathsf{CASEJUMP}}

784\newcommand{\LABEL}{\mathsf{LABEL}}

785\newcommand{\MOVE}{\mathsf{MOVE}}

786\newcommand{\JUMP}{\mathsf{JUMP}}

787\newcommand{\SPLIT}{\mathsf{SPLIT}}

788\newcommand{\SQUEEZE}{\mathsf{SQUEEZE}}

789\newcommand{\JFUN}{\mathsf{JFUN}}

790\newcommand{\PROJ}{\mathsf{PROJ}}

791\newcommand{\ERROR}{\mathsf{ERROR}}

792\newcommand{\SLIDE}{\mathsf{SLIDE}}

793\newcommand{\ALLOC}{\mathsf{ALLOC}}

794

795\newcommand{\PUSHBIG}{\mathsf{PUSHBIG}}

796\newcommand{\PUSHBASIC}{\mathsf{PUSHBASIC}}

797\newcommand{\PUSHINT}{\mathsf{PUSHINT}}

798\newcommand{\PUSHBOOL}{\mathsf{PUSHBOOL}}

799\newcommand{\GET}{\mathsf{GET}}

800\newcommand{\MKINT}{\mathsf{MKINT}}

801\newcommand{\MKBOOL}{\mathsf{MKBOOL}}

802\newcommand{\ADD}{\mathsf{ADD}}

803\newcommand{\SUB}{\mathsf{SUB}}

804\newcommand{\MULT}{\mathsf{MULT}}

805\newcommand{\LT}{\mathsf{LT}}

806\newcommand{\EQ}{\mathsf{EQ}}

807\newcommand{\GT}{\mathsf{GT}}

808\newcommand{\JTRUE}{\mathsf{JTRUE}}

809

810\newcommand{\APP}{\mathsf{APP}}

811\newcommand{\FUN}{\mathsf{FUN}}

812\newcommand{\CON}{\mathsf{CON}}

813\newcommand{\TYCON}{\mathsf{TYCON}}

814\newcommand{\TUP}{\mathsf{TUP}}

815\newcommand{\TYPE}{\mathsf{TYPE}}

816\newcommand{\INT}{\mathsf{INT}}

817\newcommand{\BIGINT}{\mathsf{BIGINT}}

818\newcommand{\BOOL}{\mathsf{BOOL}}

819\newcommand{\HOLE}{\mathsf{HOLE}}

820

821% G machine translation scheme

822

823\newcommand{\sinterp}[1]{\mathcal{S}\interp{#1}}

824\newcommand{\sinterpm}[1]{\mathcal{S}\AR{\interp{#1}}}

825\newcommand{\einterp}[3]{\mathcal{E}\interp{#1}\:#2\:#3}

826\newcommand{\cinterp}[3]{\mathcal{C}\interp{#1}\:#2\:#3}

827\newcommand{\binterp}[3]{\mathcal{B}\interp{#1}\:#2\:#3}

828\newcommand{\rinterp}[3]{\mathcal{R}\interp{#1}\:#2\:#3}

829\newcommand{\iinterp}[3]{\mathcal{I}\interp{#1}\:#2\:#3}

830\newcommand{\len}[1]{\MO{length}(#1)}

831

832\newcommand{\casecomp}[2]{\mathcal{I}(#1,\left\{\ARc{#2}\right\})}

833\newcommand{\casecompA}[3]{\mathcal{I}(#1,\left\{\ARc{#2}\right\}[#3])}

834\newcommand{\ischeme}{\mathcal{I}}

835

836% tail call markup

837

838\newcommand{\tailcall}{\mathsf{tail}}

839

840% Trees

841

842\newcommand{\Tree}{\TC{Tree}}

843\newcommand{\Leaf}{\DC{Leaf}}

844\newcommand{\Node}{\DC{Node}}

845\newcommand{\treecase}{\Cases{\Tree}}

846

847% Languages

848

849\newcommand{\Coq}{\textsc{Coq}}

850\newcommand{\Lego}{\textsc{Lego}}

851\newcommand{\Oleg}{\textsc{Oleg}}

852\newcommand{\Alf}{\textsc{Alf}}

853\newcommand{\Epigram}{\textsc{Epigram}}

854\newcommand{\SystemF}{System $\mathcal{F}$}

855\newcommand{\Iswim}{\textsc{Iswim}}

856\newcommand{\Cynthia}{\textit{C$^Y$\hspace*{-0.1cm}NTHIA}}

857

858% Accessibility

859

860\newcommand{\Acc}{\TC{Acc}}

861\newcommand{\acc}{\DC{acc}}

862\newcommand{\qsAcc}{\TC{qsAcc}}

863\newcommand{\qsNil}{\DC{qsNil}}

864\newcommand{\qsCons}{\DC{qsCons}}

865\newcommand{\allQsAcc}{\FN{allQsAcc}}

866

867% Lazy shortcuts

868

869\newcommand{\naive}{na\"{\i}ve}

870\newcommand{\Naive}{Na\"{\i}ve}

871

872% Conor's bits

873

874\newcommand{\remem}[1]{\left|#1\right|}

875\newcommand{\idsb}{\MO{id}}

876\newcommand{\ang}[1]{\langle#1\rangle}

877

878\newcommand{\vePm}[1]{\vP #1 \vm_{\Vnil} #1 \vm_{\Vcons}}%

879\newcommand{\vcrhs}{\vm_{\Vcons}\:\vk\:\va\:\vv\:%

880 (\vectelim\:\vA\:\vk\:\vv\:\vePm{\:})}%

881

882\newcommand{\igV}[2]{#1^{\ig{#2}}}

883\newcommand{\remV}[2]{#1^{\rem{#2}}}

884

885% More gubbins

886

887\newcommand{\Between}{\TC{between}}

888\newcommand{\bZ}{\DC{bO}}

889\newcommand{\bZZS}{\DC{bOOs}}

890\newcommand{\bZSS}{\DC{b0ss}}

891\newcommand{\bSSS}{\DC{bsss}}

892\newcommand{\betelim}{\Elim{\Between}}

893\newcommand{\betrhs}[1]{\motive#1\meth{\bZ}#1\meth{\bZZS}#1\meth{\bZSS}#1\meth{\bSSS}}

894

895

896\newcommand{\valenv}{\TC{ValEnv}}

897\newcommand{\vempty}{\DC{empty}}

898\newcommand{\vextend}{\DC{extend}}

899

900\newcommand{\EpiVal}{\TC{Epigram}}

901\newcommand{\unsafeCoerce}{\HF{unsafeCoerce\mbox{\texttt{\#}}}}

902

903\newcommand{\qq}{\mbox{\texttt{"}}}

904\newcommand{\impossible}{\RW{Impossible}}

905

906\newcommand{\Real}{\mathbb{R}}

907

908\newcommand{\DoubleRec}{\TC{DoubleElim}}

909\newcommand{\DoubleOn}{\DC{Double_{\Z\vn}}}

910\newcommand{\DoubleSO}{\DC{Double_{\suc\Z}}}

911\newcommand{\DoubleSS}{\DC{Double_{\suc\suc}}}

912

913\newcommand{\doublerec}{\textbf{double-elim}}

914

915\newcommand{\set}{\TC{DList}}

916\newcommand{\setuser}{\TC{DListTop}}

917\newcommand{\setempty}{\emptyset}

918\newcommand{\setinsert}{\DC{insert}}

919

920

921%%%% Type systems

922

923\newcommand{\stlc}{\lambda\hspace*{-0.15cm}\to}

924\newcommand{\plc}{\lambda2}

925\newcommand{\dlc}{\lambda{}P}

926

927\newcommand{\EC}{\mathcal{E}}

928

929%%%% reductions

930

931\newcommand{\betared}{\iq\hspace*{-0.15cm}_{\beta}}

932\newcommand{\deltared}{\iq\hspace*{-0.15cm}_{\delta}}

933\newcommand{\gammared}{\iq\hspace*{-0.15cm}_{\gamma}}

934\newcommand{\etared}{\iq\hspace*{-0.15cm}_{\eta}}

935\newcommand{\iotared}{\iq\hspace*{-0.15cm}_{\iota}}

936\newcommand{\rhored}{\iq\hspace*{-0.15cm}_{\rho}}

937

938%%%% ExTT rules

939

940\newcommand{\exconverts}{\stackrel{\mathsf{Ex}}{\converts}}

941\newcommand{\excumul}{\stackrel{\mathsf{Ex}}{\cumul}}

942\newcommand{\exequiv}{\stackrel{\mathsf{Ex}}{\equiv}}

943\newcommand{\exreduces}{\stackrel{\mathsf{Ex}}\reduces}

944\newcommand{\exreducesto}{\stackrel{\mathsf{Ex}}{\reducesto}}

945\newcommand{\exreducesn}[1]{\exreduces_{#1}}

946

947\newcommand{\ttequiv}{\stackrel{\mathsf{TT}}{\equiv}}

948\newcommand{\ttreduces}{\stackrel{\mathsf{TT}}\reduces}

949\newcommand{\ttreducesn}[1]{\ttreduces_{#1}}

950

951%%% Type synthesis

952

953\newcommand{\hastype}{\Longrightarrow}

954\newcommand{\whnfs}{\twoheadrightarrow}

955\newcommand{\conv}{\converts}

956

957\newcommand{\exhastype}{\stackrel{\mathsf{Ex}}{\hastype}}

958\newcommand{\exwhnfs}{\stackrel{\mathsf{Ex}}{\whnfs}}

959\newcommand{\exconv}{\stackrel{\mathsf{Ex}}{\conv}}

960\newcommand{\exproves}{\stackrel{\mathsf{Ex}}{\proves}}

961

962\newcommand{\tthastype}{\stackrel{\mathsf{TT}}{\hastype}}

963\newcommand{\ttwhnfs}{\stackrel{\mathsf{TT}}{\whnfs}}

964\newcommand{\ttconv}{\stackrel{\mathsf{TT}}{\conv}}

965\newcommand{\ttproves}{\stackrel{\mathsf{TT}}{\proves}}

966

967%%% Lightning

968

969\newcommand{\light}[1]{\lightning^{#1}}

970\newcommand{\LHab}[1]{\pad{\;}{:^{#1}}}

971\newcommand{\llam}[3]{\lambda#1\pad{\!}{:}^{#2}#3}

972\newcommand{\lall}[3]{\forall#1\pad{\!}{:}^{#2}#3}

973\newcommand{\lapp}[3]{#1(#2)^{#3}}

974\newcommand{\larg}[2]{(#1)^{#2}}

975

976\newcommand{\RName}[1]{\hspace*{0.1in}\mathsf{#1}}

977

978%%% LOcal macros

979

980\newcommand{\ResState}{\TC{ResourceState}}

981\newcommand{\Locked}{\DC{Locked}}

982\newcommand{\ResHandle}{\TC{ResourceHandle}}

983\newcommand{\Res}{\DC{Resource}}

984\newcommand{\CLang}{\TC{CLang}}

985\newcommand{\CFLang}{\TC{CFLang}}

986\newcommand{\CFType}{\TC{CFType}}

987\newcommand{\CLType}{\TC{CType}}

988\newcommand{\RHandle}{\DC{RHandle}}

989\newcommand{\RType}{\DC{RType}}

990\newcommand{\RUnit}{\DC{RUnit}}

991\newcommand{\LOCK}{\DC{LOCK}}

992\newcommand{\UNLOCK}{\DC{UNLOCK}}

993\newcommand{\ACTION}{\DC{ACTION}}

994\newcommand{\FORK}{\DC{FORK}}

995

996\newcommand{\FSLang}{\TC{FSLang}}

997\newcommand{\OPEN}{\DC{OPEN}}

998\newcommand{\CLOSE}{\DC{CLOSE}}

999\newcommand{\READ}{\DC{READ}}

1000\newcommand{\WRITE}{\DC{WRITE}}

1001\newcommand{\PRINT}{\DC{PRINT}}

1002\newcommand{\BIND}{\DC{BIND}}

1003

1004\newcommand{\FSType}{\TC{FSType}}

1005\newcommand{\FHandle}{\DC{FHandle}}

1006\newcommand{\FString}{\DC{FString}}

1007\newcommand{\FUnit}{\DC{FUnit}}

1008\newcommand{\ElemIs}{\TC{ElemIs}}

1009\newcommand{\elemHd}{\TC{atHead}}

1010\newcommand{\elemTl}{\TC{inTail}}

1011

1012\newcommand{\emptyEnv}{\DC{empty}}

1013\newcommand{\extendEnv}{\DC{extend}}

1014

1015\newcommand{\usera}{\FN{Alice}}

1016\newcommand{\userb}{\FN{Bob}}

1017\newcommand{\userc}{\FN{Charlie}}

1018

1019\newcommand{\FAcc}{\TC{FAcc}}

1020\newcommand{\UserA}{\DC{UserAcc}}

1021\newcommand{\GroupA}{\DC{GroupAcc}}

1022\newcommand{\GlobalA}{\DC{GlobalAcc}}

1023

1024\newcommand{\Perm}{\TC{Perm}}

1025\newcommand{\Username}{\TC{Username}}

1026\newcommand{\GroupData}{\TC{GroupData}}

1027\newcommand{\File}{\TC{File}}

1028\newcommand{\FS}{\DC{file}}

1029\newcommand{\Filepath}{\TC{Filepath}}

1030

1031\newcommand{\Read}{\DC{Read}}

1032\newcommand{\Write}{\DC{Write}}

1033\newcommand{\Execute}{\DC{Execute}}

1034

1035\newcommand{\Purpose}{\TC{Mode}}

1036\newcommand{\Reading}{\DC{Reading}}

1037\newcommand{\Writing}{\DC{Writing}}

1038

1039\newcommand{\FileState}{\TC{FileState}}

1040\newcommand{\FileHandle}{\TC{FileHandle}}

1041\newcommand{\OpenH}{\DC{OpenH}}

1042\newcommand{\ClosedH}{\DC{ClosedH}}

1043\newcommand{\Handle}{\TC{Handle}}

1044\newcommand{\Open}{\DC{Open}}

1045\newcommand{\Closed}{\DC{Closed}}

1046

1047\newcommand{\UserIO}{\TC{UserIO}}

1048\newcommand{\uio}{\DC{uio}}

1049

1050\newcommand{\CFS}{\TC{C_{fs}}}

1051\newcommand{\RFS}{\FN{R_{fs}}}

1052

1053\newcommand{\String}{\TC{String}}

1054

1055% inline idris code

1056

1057\newcommand{\Tcon}[1]{\texttt{#1}}

1058\newcommand{\Dcon}[1]{\texttt{#1}}

1059\newcommand{\Fname}[1]{\texttt{#1}}

1060\newcommand{\Vv}[1]{\texttt{#1}}

1061\newcommand{\TyTy}{\texttt{\#}}

1062

1063\newcommand{\direct}[1]{\texttt{\%#1}}

1064

1065\newcommand{\Feature}[1]{\textbf{Remark:}}

1066%\newcommand{\Remark}[1]{\textbf{Remark:}}