Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Started a new tutorial. Don't hold your breath.

  • Loading branch information...
commit 8fbef4215faca589098a2e544a2d351eef9e2d57 1 parent dea8d48
Edwin Brady authored
View
41 tutorial/Makefile
@@ -0,0 +1,41 @@
+PAPER = idris-tutorial
+
+all: ${PAPER}.pdf
+
+TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex
+
+DIAGS =
+
+SOURCES = ${TEXFILES} ${DIAGS} macros.ltx library.ltx literature.bib
+
+DITAA = java -jar ~/Downloads/ditaa.jar
+
+${PAPER}.pdf: ${SOURCES}
+# dvipdf ${PAPER}.dvi
+ pdflatex ${PAPER}
+ -bibtex ${PAPER}
+ -pdflatex ${PAPER}
+ -pdflatex ${PAPER}
+
+${PAPER}.ps: ${PAPER}.dvi
+ dvips -o ${PAPER}.ps ${PAPER}
+
+${PAPER}.dvi: $(SOURCES)
+ -latex ${PAPER}
+ -bibtex ${PAPER}
+ -latex ${PAPER}
+ -latex ${PAPER}
+
+progress: .PHONY
+ wc -w ${TEXFILES}
+
+%.png : %.diag
+ $(DITAA) -o -E $<
+
+todropbox: .PHONY
+ cp ${SOURCES} ~/Dropbox/TeX/ImplDTP/
+
+fromdropbox: .PHONY
+ cp ~/Dropbox/TeX/ImplDTP/* .
+
+.PHONY:
View
5 tutorial/examples/hello.idr
@@ -0,0 +1,5 @@
+module main;
+
+main : IO ();
+main = putStrLn "Hello world";
+
View
40 tutorial/idris-tutorial.tex
@@ -0,0 +1,40 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\usepackage{palatino}
+\usepackage{url}
+\usepackage{fancyvrb}
+
+\input{macros.ltx}
+\input{library.ltx}
+
+\newcommand{\Idris}{\textsc{Idris}}
+
+\title{Dependently Typed Programming in \Idris{}}
+\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
+
+\begin{document}
+
+\maketitle
+
+%\tableofcontents
+
+\input{intro}
+\input{starting}
+
+%Planned sections
+
+\section{Types and Functions}
+\section{Type Classes}
+\section{The Well-Typed Interpreter}
+\section{Views}
+\section{Theorem Proving}
+\section{Provisional Definitions}
+\section{A verified binary adder}
+
+\input{miscellany}
+
+\bibliographystyle{abbrv}
+\bibliography{literature.bib}
+
+\end{document}
View
56 tutorial/intro.tex
@@ -0,0 +1,56 @@
+\section{Introduction}
+
+In conventional programming languages, there is a clear distinction between
+\remph{types} and \remph{values}. For example, in Haskell~\cite{haskell-report},
+the following are types, representing integers, characters, lists of characters,
+and lists of any value respectively:
+
+\begin{itemize}
+\item \texttt{Int}, \texttt{Char}, \texttt{[Char]}, \texttt{[a]}
+\end{itemize}
+
+\noindent
+Correspondingly, the following values are examples of inhabitants of those types:
+
+\begin{itemize}
+\item \texttt{42}, \texttt{'a'}, \texttt{"Hello world!"}, \texttt{[2,3,4,5,6]}
+\end{itemize}
+
+In a language with \emph{dependent types}, however, the distinction is less
+clear. Dependent types allow types to ``depend'' on values. The standard
+example is the type of lists of a given length\footnote{Typically, and perhaps
+confusingly, referred to in the dependently typed programming literaute as
+``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and
+\texttt{n} is the length of the list and can be an arbitrary
+term.
+
+When types can contain values, and where those values describe properties (e.g.
+the length of a list)
+functions over those types begin to describe their own properties. For example,
+concatenating two lists has the property that the resulting list's length is
+the sum of the lengths of the two input lists. We can therefore give the following type
+to the \texttt{app} function, which concatenates vectors:
+
+\begin{SaveVerbatim}{appendv}
+
+app : Vect a n -> Vect a m -> Vect a (n + m);
+
+\end{SaveVerbatim}
+\useverb{appendv}
+
+
+This tutorial introduces \Idris{}, a general purpose dependently typed functional
+programming language.
+The goal of the \Idris{} project is to build a dependently typed language suitable
+for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
+which aims to generate efficient executable code. It also has a lightweight foreign
+function interface which allows easy interaction with external C libraries.
+
+\subsection{Intended Audience}
+
+This tutorial is intended as a brief introduction to the language, and is aimed
+at readers already familiar with a functional language such as Haskell or
+OCaml. In particular, a certain amount of familiarity with Haskell syntax is
+assumed, although most concepts will at least be explained briefly. The reader
+is also assumed to have some interest in using dependent types for writing and
+verifying systems software.
View
325 tutorial/library.ltx
@@ -0,0 +1,325 @@
+%%%%%%%%%%%%%%% library file for datatypes etc.
+
+%%% Identifiers
+
+\newcommand{\va}{\VV{a}}
+\newcommand{\vb}{\VV{b}}
+\newcommand{\vc}{\VV{c}}
+\newcommand{\vd}{\VV{d}}
+\newcommand{\ve}{\VV{e}}
+\newcommand{\vf}{\VV{f}}
+\newcommand{\vg}{\VV{g}}
+\newcommand{\vh}{\VV{h}}
+\newcommand{\vi}{\VV{i}}
+\newcommand{\vj}{\VV{j}}
+\newcommand{\vk}{\VV{k}}
+\newcommand{\vl}{\VV{l}}
+\newcommand{\vm}{\VV{m}}
+\newcommand{\vn}{\VV{n}}
+\newcommand{\vo}{\VV{o}}
+\newcommand{\vp}{\VV{p}}
+\newcommand{\vq}{\VV{q}}
+\newcommand{\vr}{\VV{r}}
+\newcommand{\vs}{\VV{s}}
+\newcommand{\vt}{\VV{t}}
+\newcommand{\vu}{\VV{u}}
+\newcommand{\vv}{\VV{v}}
+\newcommand{\vw}{\VV{w}}
+\newcommand{\vx}{\VV{x}}
+\newcommand{\vy}{\VV{y}}
+\newcommand{\vz}{\VV{z}}
+\newcommand{\vA}{\VV{A}}
+\newcommand{\vB}{\VV{B}}
+\newcommand{\vC}{\VV{C}}
+\newcommand{\vD}{\VV{D}}
+\newcommand{\vE}{\VV{E}}
+\newcommand{\vF}{\VV{F}}
+\newcommand{\vG}{\VV{G}}
+\newcommand{\vH}{\VV{H}}
+\newcommand{\vI}{\VV{I}}
+\newcommand{\vJ}{\VV{J}}
+\newcommand{\vK}{\VV{K}}
+\newcommand{\vL}{\VV{L}}
+\newcommand{\vM}{\VV{M}}
+\newcommand{\vN}{\VV{N}}
+\newcommand{\vO}{\VV{O}}
+\newcommand{\vP}{\VV{P}}
+\newcommand{\vQ}{\VV{Q}}
+\newcommand{\vR}{\VV{R}}
+\newcommand{\vS}{\VV{S}}
+\newcommand{\vT}{\VV{T}}
+\newcommand{\vU}{\VV{U}}
+\newcommand{\vV}{\VV{V}}
+\newcommand{\vW}{\VV{W}}
+\newcommand{\vX}{\VV{X}}
+\newcommand{\vY}{\VV{Y}}
+\newcommand{\vZ}{\VV{Z}}
+\newcommand{\vas}{\VV{as}}
+\newcommand{\vbs}{\VV{bs}}
+\newcommand{\vcs}{\VV{cs}}
+\newcommand{\vds}{\VV{ds}}
+\newcommand{\ves}{\VV{es}}
+\newcommand{\vfs}{\VV{fs}}
+\newcommand{\vgs}{\VV{gs}}
+\newcommand{\vhs}{\VV{hs}}
+\newcommand{\vis}{\VV{is}}
+\newcommand{\vjs}{\VV{js}}
+\newcommand{\vks}{\VV{ks}}
+\newcommand{\vls}{\VV{ls}}
+\newcommand{\vms}{\VV{ms}}
+\newcommand{\vns}{\VV{ns}}
+\newcommand{\vos}{\VV{os}}
+\newcommand{\vps}{\VV{ps}}
+\newcommand{\vqs}{\VV{qs}}
+\newcommand{\vrs}{\VV{rs}}
+%\newcommand{\vss}{\VV{ss}}
+\newcommand{\vts}{\VV{ts}}
+\newcommand{\vus}{\VV{us}}
+\newcommand{\vvs}{\VV{vs}}
+\newcommand{\vws}{\VV{ws}}
+\newcommand{\vxs}{\VV{xs}}
+\newcommand{\vys}{\VV{ys}}
+\newcommand{\vzs}{\VV{zs}}
+
+%%% Telescope Identifiers
+
+\newcommand{\ta}{\vec{\VV{a}}}
+\newcommand{\tb}{\vec{\VV{b}}}
+\newcommand{\tc}{\vec{\VV{c}}}
+\newcommand{\td}{\vec{\VV{d}}}
+\newcommand{\te}{\vec{\VV{e}}}
+\newcommand{\tf}{\vec{\VV{f}}}
+\newcommand{\tg}{\vec{\VV{g}}}
+%\newcommand{\th}{\vec{\VV{h}}}
+\newcommand{\ti}{\vec{\VV{i}}}
+\newcommand{\tj}{\vec{\VV{j}}}
+\newcommand{\tk}{\vec{\VV{k}}}
+\newcommand{\tl}{\vec{\VV{l}}}
+\newcommand{\tm}{\vec{\VV{m}}}
+\newcommand{\tn}{\vec{\VV{n}}}
+%\newcommand{\to}{\vec{\VV{o}}}
+\newcommand{\tp}{\vec{\VV{p}}}
+\newcommand{\tq}{\vec{\VV{q}}}
+\newcommand{\tr}{\vec{\VV{r}}}
+\newcommand{\tts}{\vec{\VV{s}}}
+\newcommand{\ttt}{\vec{\VV{t}}}
+\newcommand{\tu}{\vec{\VV{u}}}
+%\newcommand{\tv}{\vec{\VV{v}}}
+\newcommand{\tw}{\vec{\VV{w}}}
+\newcommand{\tx}{\vec{\VV{x}}}
+\newcommand{\ty}{\vec{\VV{y}}}
+\newcommand{\tz}{\vec{\VV{z}}}
+\newcommand{\tA}{\vec{\VV{A}}}
+\newcommand{\tB}{\vec{\VV{B}}}
+\newcommand{\tC}{\vec{\VV{C}}}
+\newcommand{\tD}{\vec{\VV{D}}}
+\newcommand{\tE}{\vec{\VV{E}}}
+\newcommand{\tF}{\vec{\VV{F}}}
+\newcommand{\tG}{\vec{\VV{G}}}
+\newcommand{\tH}{\vec{\VV{H}}}
+\newcommand{\tI}{\vec{\VV{I}}}
+\newcommand{\tJ}{\vec{\VV{J}}}
+\newcommand{\tK}{\vec{\VV{K}}}
+\newcommand{\tL}{\vec{\VV{L}}}
+\newcommand{\tM}{\vec{\VV{M}}}
+\newcommand{\tN}{\vec{\VV{N}}}
+\newcommand{\tO}{\vec{\VV{O}}}
+\newcommand{\tP}{\vec{\VV{P}}}
+\newcommand{\tQ}{\vec{\VV{Q}}}
+\newcommand{\tR}{\vec{\VV{R}}}
+\newcommand{\tS}{\vec{\VV{S}}}
+\newcommand{\tT}{\vec{\VV{T}}}
+\newcommand{\tU}{\vec{\VV{U}}}
+\newcommand{\tV}{\vec{\VV{V}}}
+\newcommand{\tW}{\vec{\VV{W}}}
+\newcommand{\tX}{\vec{\VV{X}}}
+\newcommand{\tY}{\vec{\VV{Y}}}
+\newcommand{\tZ}{\vec{\VV{Z}}}
+
+
+
+%%% Nat
+
+\newcommand{\NatPackage}{
+ \newcommand{\Nat}{\TC{\mathbb{N}}}
+ \newcommand{\Z}{\DC{0}}
+ \newcommand{\suc}{\DC{s}}
+ \newcommand{\NatDecl}{
+ \Data \hg
+ \Axiom{\Nat\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\Z\Hab\Nat} \hg
+ \Rule{\vn\Hab\Nat}
+ {\suc\:\vn\Hab\Nat}
+}}
+
+%%% Bool
+
+\newcommand{\BoolPackage}{
+ \newcommand{\Bool}{\TC{Bool}}
+ \newcommand{\true}{\DC{true}}
+ \newcommand{\false}{\DC{false}}
+ \newcommand{\BoolDecl}{
+ \Data \hg
+ \Axiom{\Bool\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\true\Hab\Bool} \hg
+ \Axiom{\false\Hab\Bool}
+}}
+
+%%% So
+
+\newcommand{\SoPackage}{
+ \newcommand{\So}{\TC{So}}
+ \newcommand{\oh}{\DC{oh}}
+ \newcommand{\SoDecl}{
+ \Data \hg
+ \Rule{\vb\Hab\Bool}
+ {\So\:\vb\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\oh\Hab\So\:\true}
+}}
+
+%%% Unit
+
+\newcommand{\UnitPackage}{
+ \newcommand{\Unit}{\TC{Unit}}
+ \newcommand{\void}{\DC{void}}
+ \newcommand{\UnitDecl}{
+ \Data \hg
+ \Axiom{\Unit\Hab\Type} \hg
+ \Where \hg
+ \Axiom{\void\Hab\Unit}
+}}
+
+%%% Maybe
+
+\newcommand{\MaybePackage}{
+ \newcommand{\Maybe}{\TC{Maybe}}
+ \newcommand{\yes}{\DC{yes}}
+ \newcommand{\no}{\DC{no}}
+ \newcommand{\MaybeDecl}{
+ \Data \hg
+ \Rule{\vA\Hab\Type}
+ {\Maybe\:\vA\Hab\Type} \hg
+ \Where \hg
+ \Rule{\va \Hab \vA}
+ {\yes\:\va\Hab\Maybe\:\vA} \hg
+ \Axiom{\no\Hab\Maybe\:\vA}
+}}
+
+%%% Cross
+
+\newcommand{\pr}[2]{(#1\DC{,}#2)} %grrrr
+\newcommand{\CrossPackage}{
+ \newcommand{\Cross}{\times}
+ \newcommand{\CrossDecl}{
+ \Data \hg
+ \Rule{\vA,\vB\Hab\Type}
+ {\vA\Cross\vB\Hab\Type} \hg
+ \Where \hg
+ \Rule{\va \Hab \vA \hg \vb\Hab\vB}
+ {\pr{\va}{\vb}\Hab\vA\Cross\vB}
+}}
+
+%%% Fin
+
+\newcommand{\FinPackage}{
+ \newcommand{\Fin}{\TC{Fin}}
+ \newcommand{\fz}{\DC{f0}}
+ \newcommand{\fs}{\DC{fs}}
+ \newcommand{\FinDecl}{
+ \AR{
+ \Data \hg
+ \Rule{\vn\Hab\Nat}
+ {\Fin\:\vn\Hab\Type} \hg \\
+ \Where \hg
+ \begin{array}[t]{c}
+ \Axiom{\fz\Hab\Fin\:(\suc\:\vn)} \hg
+ \Rule{\vi\Hab\Fin\:\vn}
+ {\fs\:\vi\Hab\Fin\:(\suc\:\vn)}
+ \end{array}
+ }
+}}
+
+%%% Vect
+
+\newcommand{\VectPackage}{
+ \newcommand{\Vect}{\TC{Vect}}
+ \newcommand{\vnil}{\varepsilon}
+ \newcommand{\vcons}{\,\dcolon\,}
+ \newcommand{\vsnoc}{\,\dcolon\,}
+ \newcommand{\VectConsDecl}{
+ \Data \hg
+ \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
+ {\Vect\:\vA\:\vn\Hab\Type} \hg
+ \Where \hg \begin{array}[t]{c}
+ \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
+ \Rule{\vx\Hab\vA \hg \vxs\Hab \Vect\:\vA\:\vn }
+ {\vx\vcons\vxs\Hab\Vect\:\vA\:(\suc\vn)}
+ \end{array}
+}
+ \newcommand{\VectSnocDecl}{
+ \Data \hg
+ \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
+ {\Vect\:\vA\:\vn\Hab\Type} \hg
+ \Where \hg \begin{array}[t]{c}
+ \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
+ \Rule{\vxs\Hab \Vect\:\vA\:\vn \hg \vx\Hab\vA}
+ {\vxs\vsnoc\vx\Hab\Vect\:\vA\:(\suc\vn)}
+ \end{array}
+}
+}
+
+%%% Compare
+
+%Data Compare : (x:nat)(y:nat)Type
+% = lt : (x:nat)(y:nat)(Compare x (plus (S y) x))
+% | eq : (x:nat)(Compare x x)
+% | gt : (x:nat)(y:nat)(Compare (plus (S x) y) y);
+
+
+\newcommand{\ComparePackage}{
+ \newcommand{\Compare}{\TC{Compare}}
+ \newcommand{\ltComp}{\DC{lt}}
+ \newcommand{\eqComp}{\DC{eq}}
+ \newcommand{\gtComp}{\DC{gt}}
+ \newcommand{\CompareDecl}{
+ \Data \hg
+ \Rule{\vm\Hab\Nat\hg\vn\Hab\Nat}
+ {\Compare\:\vm\:\vn\Hab\Type} \\
+ \Where \hg\begin{array}[t]{c}
+ \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
+ {\ltComp_{\vx}\:\vy\Hab\Compare\:\vx\:(\FN{plus}\:\vx\:(\suc\:\vy))} \\
+ \Rule{\vx\Hab\Nat}
+ {\eqComp_{\vx}\Hab\Compare\:\vx\:\vx}\\
+ \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
+ {\gtComp_{\vy}\:\vx\Hab\Compare\:(\FN{plus}\:\vy\:(\suc\:\vx))\:\vy} \\
+ \end{array}
+ }
+
+%Data CompareM : Type
+% = ltM : (ydiff:nat)CompareM
+% | eqM : CompareM
+% | gtM : (xdiff:nat)CompareM;
+
+ \newcommand{\CompareM}{\TC{Compare^-}}
+ \newcommand{\ltCompM}{\DC{lt^-}}
+ \newcommand{\eqCompM}{\DC{eq^-}}
+ \newcommand{\gtCompM}{\DC{gt^-}}
+ \newcommand{\CompareMDecl}{
+
+ \Data \hg
+ \Axiom{\CompareM\Hab\Type} \\
+ \Where \hg\begin{array}[t]{c}
+ \Rule{\vy\Hab\Nat}
+ {\ltCompM\:\vy\Hab\CompareM} \\
+ \Axiom{\eqCompM\Hab\CompareM}\\
+ \Rule{\vx\Hab\Nat}
+ {\gtCompM\:\vx\Hab\CompareM} \\
+ \end{array}
+ }
+ \newcommand{\CompareRec}{\FN{CompareRec}}
+ \newcommand{\CompareRecM}{\FN{CompareRec^-}}
+
+}
View
3,846 tutorial/literature.bib
3,846 additions, 0 deletions not shown
View
1,062 tutorial/macros.ltx
@@ -0,0 +1,1062 @@
+%\usepackage{amstex}
+\usepackage{amssymb}
+\usepackage{latexsym}
+\usepackage{eepic}
+
+
+%%%%%%%%% INFERENCE RULES
+
+\newlength{\rulevgap}
+\setlength{\rulevgap}{0.05in}
+\newlength{\ruleheight}
+\newlength{\ruledepth}
+\newsavebox{\rulebox}
+\newlength{\GapLength}
+\newcommand{\gap}[1]{\settowidth{\GapLength}{#1} \hspace*{\GapLength}}
+\newcommand{\dotstep}[2]{\begin{tabular}[b]{@{}c@{}}
+ #1\\$\vdots$\\#2
+ \end{tabular}}
+\newlength{\fracwid}
+\newcommand{\dotfrac}[2]{\settowidth{\fracwid}{$\frac{#1}{#2}$}
+ \addtolength{\fracwid}{0.1in}
+ \begin{tabular}[b]{@{}c@{}}
+ $#1$\\
+ \parbox[c][0.02in][t]{\fracwid}{\dotfill} \\
+ $#2$\\
+ \end{tabular}}
+\newcommand{\Rule}[2]{\savebox{\rulebox}[\width][b] %
+ {\( \frac{\raisebox{0in} {\( #1 \)}} %
+ {\raisebox{-0.03in}{\( #2 \)}} \)} %
+ \settoheight{\ruleheight}{\usebox{\rulebox}} %
+ \addtolength{\ruleheight}{\rulevgap} %
+ \settodepth{\ruledepth}{\usebox{\rulebox}} %
+ \addtolength{\ruledepth}{\rulevgap} %
+ \raisebox{0in}[\ruleheight][\ruledepth] %
+ {\usebox{\rulebox}}}
+\newcommand{\Case}[2]{\savebox{\rulebox}[\width][b] %
+ {\( \dotfrac{\raisebox{0in} {\( #1 \)}} %
+ {\raisebox{-0.03in}{\( #2 \)}} \)} %
+ \settoheight{\ruleheight}{\usebox{\rulebox}} %
+ \addtolength{\ruleheight}{\rulevgap} %
+ \settodepth{\ruledepth}{\usebox{\rulebox}} %
+ \addtolength{\ruledepth}{\rulevgap} %
+ \raisebox{0in}[\ruleheight][\ruledepth] %
+ {\usebox{\rulebox}}}
+\newcommand{\Axiom}[1]{\savebox{\rulebox}[\width][b] %
+ {$\frac{}{\raisebox{-0.03in}{$#1$}}$} %
+ \settoheight{\ruleheight}{\usebox{\rulebox}} %
+ \addtolength{\ruleheight}{\rulevgap} %
+ \settodepth{\ruledepth}{\usebox{\rulebox}} %
+ \addtolength{\ruledepth}{\rulevgap} %
+ \raisebox{0in}[\ruleheight][\ruledepth] %
+ {\usebox{\rulebox}}}
+\newcommand{\RuleSide}[3]{\gap{$#2$} \hspace*{0.1in} %
+ \Rule{#1}{#3} %
+ \hspace*{0.1in}$#2$}
+\newcommand{\AxiomSide}[2]{\gap{$#1$} \hspace*{0.1in} %
+ \Axiom{#2} %
+ \hspace*{0.1in}$#1$}
+\newcommand{\RULE}[1]{\textbf{#1}}
+\newcommand{\hg}{\hspace{0.2in}}
+
+\newcommand{\ProofState}
+ [2]{\parbox{10cm}{\AR{\hg\AR{#1}\\\Axiom{\hg#2\hg}}}}
+
+%%%%%%%%%%%% TRISTUFF
+
+\newcommand{\btr}{
+\setlength{\unitlength}{0.0005in}
+\begin{picture}(69,180)(0,12)
+\blacken\path(57,192)(57,12)(12,102)
+ (57,192)(57,192)
+\path(57,192)(57,12)(12,102)
+ (57,192)(57,192)
+\end{picture}
+}
+
+\newcommand{\btl}{
+\setlength{\unitlength}{0.0005in}
+\begin{picture}(69,180)(0,12)
+\blacken\path(12,192)(12,12)(57,102)
+ (12,192)(12,192)
+\path(12,192)(12,12)(57,102)
+ (12,192)(12,192)
+\end{picture}
+}
+
+\newcommand{\wtr}{
+\setlength{\unitlength}{0.0005in}
+\begin{picture}(69,180)(0,12)
+%\blacken\path(57,192)(57,12)(12,102)
+% (57,192)(57,192)
+\path(57,192)(57,12)(12,102)
+ (57,192)(57,192)
+\end{picture}
+}
+
+\newcommand{\wtl}{
+\setlength{\unitlength}{0.0005in}
+\begin{picture}(69,180)(0,12)
+%\blacken\path(12,192)(12,12)(57,102)
+% (12,192)(12,192)
+\path(12,192)(12,12)(57,102)
+ (12,192)(12,192)
+\end{picture}
+}
+
+
+
+%%%%%%%%%%%% FONTS
+
+\newcommand{\TC}[1]{\mathsf{#1}}
+\newcommand{\DC}[1]{\mathsf{#1}}
+\newcommand{\VV}[1]{\mathit{#1}}
+\newcommand{\FN}[1]{\mathbf{#1}}
+\newcommand{\HFN}[1]{\mathtt{#1}}
+\newcommand{\RW}[1]{\underline{\textrm{#1}}}
+\newcommand{\MO}[1]{\mbox{\textsc{#1}}}
+
+\newcommand{\HF}[1]{\mathtt{#1}}
+
+\newcommand{\MV}[1]{\nhole\mathit{#1}}
+\newcommand{\Lang}[1]{\mathsf{#1}}
+\newcommand{\Name}[1]{\mathit{#1}}
+
+\newcommand{\demph}[1]{\textbf{#1}}
+\newcommand{\remph}[1]{\emph{#1}}
+
+%%%% Keywords for meta operations
+\newcommand{\IF}{\;\RW{if}\;\;}
+\newcommand{\THEN}{\RW{then}}
+\newcommand{\ELSE}{\RW{else}}
+\newcommand{\AND}{\RW{and}}
+\newcommand{\Otherwise}{\RW{otherwise}}
+\newcommand{\Do}{\RW{do}}
+\newcommand{\Return}{\RW{return}}
+
+\newcommand{\CASE}{\RW{case}}
+\newcommand{\LET}{\RW{let}}
+\newcommand{\IN}{\RW{in}}
+\newcommand{\of}{\RW{of}}
+
+\newcommand{\CLASS}{\mathtt{class}}
+\newcommand{\INSTANCE}{\mathtt{instance}}
+
+%%%%%%%%%%%% GROUPING
+
+\newcommand{\G}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\path(2,10)(2,-10)
+\end{picture}
+}
+
+\newcommand{\E}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\path(2,10)(2,-2)(4,-2)
+\end{picture}
+}
+
+%\newcommand{\C}{
+%\setlength{\unitlength}{1pt}
+%\begin{picture}(4,10)(0,0)
+%\path(4,8)(2,8)(2,-2)(4,-2)
+%\end{picture}
+%}
+
+\newcommand{\M}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\path(2,10)(2,-2)(6,-2)
+\end{picture}
+}
+
+\newcommand{\F}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\path(4,8)(2,8)(2,-6)
+\end{picture}
+}
+
+\newcommand{\K}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\path(0,8)(4,8)
+\end{picture}
+}
+
+\newcommand{\J}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\path(0,-2)(4,-2)
+\end{picture}
+}
+
+\newcommand{\W}{
+\setlength{\unitlength}{1pt}
+\begin{picture}(4,10)(0,0)
+\end{picture}
+}
+
+
+
+%%%%%%%%%%%% GUBBINS
+
+\newcommand{\mathskip}{\medskip}
+
+\newcommand{\fbx}[1]{\fbox{$#1$}}
+\newcommand{\stk}[1]{\begin{array}{c}#1\end{array}}
+%\newcommand{\DM}[1]{\hg\mbox{$#1$}}
+\newcommand{\DM}[1]{\mathskip\par\(#1\)\mathskip}
+\newcommand{\mbx}[1]{\mathskip\par\noindent\(#1\)\mathskip}
+\newcommand{\AR}[1]{\begin{array}[t]{@{}l}#1\end{array}}
+\newcommand{\ARt}[1]{\begin{array}[t]{@{}l@{}cl}#1\end{array}}
+\newcommand{\ARc}[1]{\begin{array}{@{}l}#1\end{array}}
+\newcommand{\ARd}[1]{\begin{array}[t]{cl}#1\end{array}}
+\newcommand{\DAR}[1]{\begin{array}{ll}\hg & #1\end{array}}
+\newcommand{\Dor}{\\ \hg\mid & }
+\newcommand{\EA}[1]{\begin{array}[t]{r@{}c@{}l}#1\end{array}}
+\newcommand{\A}{@{\:}c}
+%\newcommand{\R}{@{\:}r}
+\newcommand{\CA}{c}
+\newcommand{\LA}{l}
+\newcommand{\PAc}[2]{\begin{array}{l#1@{}r@{}l}#2\end{array}}
+\newcommand{\PA}[2]{\begin{array}[t]{l@{\:}l#1@{}r@{\:}l}#2\end{array}}
+\newcommand{\DTREE}[3]{\begin{array}[t]{l#1@{}r@{\:}l#2}#3\end{array}}
+\newcommand{\IDTREE}[2]{%
+ \begin{array}[t]{l@{\:}c@{\:}l@{\:}r@{\:}l#1}#2\end{array}}
+\newcommand{\IA}[2]
+ {\begin{array}[t]{l@{\:}r@{\:}c@{\:}l@{\:}#1@{\:}r@{\:}l}#2\end{array}}
+\newcommand{\IAc}[2]
+ {\begin{array}[c]{r@{\:}c@{\:}l@{\:}#1@{}r@{}l}#2\end{array}}
+\newcommand{\CS}[1]{\left\lfloor\begin{array}{@{}l}#1\end{array}\right.}
+\newcommand{\BY}[3]{\multicolumn{2}{l}{\;\RW{by}\; #1} \\ %
+ \multicolumn{#2}{l}{\CS{#3}} }
+\newcommand{\WITH}[3]{\multicolumn{2}{l}{\;\RW{with}\; #1} \\ %
+ \multicolumn{#2}{l}{\CS{#3}} }
+\newcommand{\WithBy}{\RW{with-by}}
+\newcommand{\Wb}[1]{\WithBy& #1}
+\newcommand{\By}[1]{\multicolumn{2}{l}{\Leftarrow #1}}
+\newcommand{\andby}{\Leftarrow}
+\newcommand{\MyWith}[1]{\multicolumn{2}{l}{|\;#1}}
+\newcommand{\Byr}[1]{\;\RW{by}\; #1}
+
+\newcommand{\Bar}{|}
+\newcommand{\Bart}{\settowidth{\GapLength}{$\Bar$}%
+ \raisebox{6pt}[0pt][0pt]{$\Bar$}%
+ \hspace*{-1\GapLength}%
+ \Bar}
+\newcommand{\With}[1]{\Bar & #1}
+\newcommand{\Witt}[1]{\Bart & #1}
+
+\newcommand{\B}{@{\:}r@{\:}c}
+\newcommand{\Ret}[1]{\multicolumn{2}{l}{\cq #1}}
+\newcommand{\MRet}[2]{\multicolumn{#1}{l}{\cq #2}}
+\newcommand{\HRet}[1]{\multicolumn{2}{l}{\hq #1}}
+\newcommand{\MHRet}[2]{\multicolumn{#1}{l}{\hq #2}}
+\newcommand{\IRet}[1]{\multicolumn{2}{l}{\iq #1}}
+\newcommand{\IMRet}[2]{\multicolumn{#1}{l}{\iq #2}}
+\newcommand{\MoRet}[1]{\multicolumn{2}{l}{\mq #1}}
+\newcommand{\MMoRet}[2]{\multicolumn{#1}{l}{\mq #2}}
+\newcommand{\Data}{\RW{data}}
+\newcommand{\Codata}{\RW{codata}}
+\newcommand{\Where}{\RW{where}}
+\newcommand{\Let}{\RW{let}}
+\newcommand{\Fact}{\RW{fact}}
+\newcommand{\Rec}[1]{#1\textbf{-Rec}}
+\newcommand{\Memo}[1]{#1\textbf{-Memo}}
+\newcommand{\Elim}[1]{#1\textbf{-Elim}}
+\newcommand{\Cases}[1]{#1\textbf{-Case}}
+\newcommand{\View}[1]{#1\textbf{-View}}
+\newcommand{\As}[2]{#1 \:\RW{as}\: #2}
+\newcommand{\nhole}{\Box}
+\newcommand{\turq}{\:\vdash_?\:}
+\newcommand{\split}{\;\lhd\;}
+\newcommand{\CType}[2]{\{#1 \split\; #2\}}
+\newcommand{\CC}[2]{(#1)\:#2}
+\newcommand{\UP}[2]{#1 | \{#2\}}
+\newcommand{\Ured}{\:\Downarrow\:}
+\newcommand{\gdd}{\prec}
+\newcommand{\HC}[1]{\left<#1\right>}
+\newcommand{\HT}[2]{\left<#1 \hab #2\right>}
+
+\newcommand{\view}{\RW{view}}
+\newcommand{\ecase}{\RW{case}}
+\newcommand{\rec}{\RW{rec}}
+
+\newcommand{\If}{\mathsf{if}}
+\newcommand{\Then}{\mathsf{then}}
+\newcommand{\Else}{\mathsf{else}}
+\newcommand{\elim}{\RW{elim}}
+
+\newcommand{\Payload}{\mathsf{type}}
+\newcommand{\Any}{\mathsf{Some}}
+
+\newcommand{\lbl}[2]{\langle #1 \Hab #2 \rangle}
+\newcommand{\call}[2]{\RW{call}\:\langle#1\rangle\:#2}
+\newcommand{\return}[1]{\RW{return}\:#1}
+
+\newcommand{\Remark}[1]{\noindent\textbf{Remark:} #1}
+
+\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}
+
+\newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}
+\newcommand{\useverb}[1]{\BUseVerbatim{#1}}
+\newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
+\newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
+
+\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}
+\caption{#3}\label{#2}\end{figure}}
+\newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
+\newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}
+\newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
+\newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
+\newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
+\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}
+\caption{#3}\label{#2}\end{figure*}}
+
+\newcommand{\FIG}[3]{\begin{figure}[h]\DM{#1}\caption{#2}\label{#3}\end{figure}}
+\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
+\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
+\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}
+\newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}
+\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}
+\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
+
+\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}
+\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}
+
+\newcommand{\RESFIG}[3]{
+\TFIG{|l|c|c|c|c|c|c|c|c|}{
+\hline
+ & \multicolumn{4}{c|}{\Naive{} compilation} &
+ \multicolumn{4}{|c|}{Optimised compilation} \\
+\cline{2-9}
+\raisebox{1.5ex}[0pt]{Program} & Instrs & Thunks & Cells &
+Accesses & Instructions & Thunks & Cells & Accesses \\
+%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
+\hline
+#1
+\hline
+}{#2}{#3}}
+
+\newcommand{\NEWRESFIG}[3]{
+\TFIG{|l|l|c|c|c|c|}{
+\hline
+% & \multicolumn{4}{c|}{\Naive{} compilation} &
+% \multicolumn{4}{|c|}{Optimised compilation} \\
+%\cline{2-9}
+Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
+%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
+\hline
+#1
+}{#2}{#3}}
+
+\newcommand{\NEWRESFIGTC}[3]{
+\TFIGTC{|l|l|c|c|c|c|}{
+\hline
+% & \multicolumn{4}{c|}{\Naive{} compilation} &
+% \multicolumn{4}{|c|}{Optimised compilation} \\
+%\cline{2-9}
+Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
+%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
+\hline
+#1
+}{#2}{#3}}
+
+\newcommand{\RESLINE}[9]{
+& \Naive{} & #2 & #3 & #5 & #4 \\
+#1
+& Optimised & #6 & #7 & #9 & #8 \\
+}
+\newcommand{\RESCHANGE}[4]{
+& Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\
+\hline
+}
+\newcommand{\RESCHANGEa}[5]{
+#5 & Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\
+\hline
+}
+
+%%%%%%%%%%%% PUNCTUATION
+
+\newcommand{\pad}[2]{#1#2#1}
+
+\newcommand{\hab}{\pad{\,}{:}}
+\newcommand{\Hab}{\pad{\;}{:}}
+\newcommand{\HHab}{\pad{\;}{::}}
+
+%%%%%%%%%%%% TYPE
+
+\newcommand{\Type}{\mbox{\texttt{\#}}} %\star}
+
+
+%%%%%%%%%%%%% ARROWS
+
+\newcommand{\To}{\pad{\:}{\rightarrow}}
+\newcommand{\Gets}{\leftarrow}
+%\newcommand{\car}{\vartriangleright}
+
+%%%%%%%%%%%%% QUANTIFIERS
+
+\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}
+\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}
+\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}
+\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}
+\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}
+\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}
+\newcommand{\remall}[2]{\forall\{#1\pad{\!}{:}#2\}}
+\newcommand{\allpi}[2]{\Pi#1\pad{\!}{:}#2}
+\newcommand{\ali}[2]{\forall#1|#2}
+\newcommand{\exi}[2]{\exists#1\pad{\!}{:}#2}
+\newcommand{\wit}[2]{\ang{#1,#2}}
+\newcommand{\X}{\times}
+\newcommand{\sig}[2]{\Sigma#1\pad{\!}{:}#2}
+
+\newcommand{\SC}{.\:}
+
+\newcommand{\letbind}[3]{\mathsf{let}\:#1{:}#2\:=\:#3\:\mathsf{in}}
+\newcommand{\ifthen}[3]{\mathsf{if}\:#1\:\mathsf{then}\:#2\:\mathsf{else}\:#3}
+
+%%%%%%%%%%%%% EQUALITIES
+
+\newcommand{\cq}{\pad{\:}{\mapsto}}
+\newcommand{\xq}{\pad{}{\doteq}}
+\newcommand{\pq}{\pad{\:}{=}}
+\newcommand{\dq}{\pad{\:}{:=}}
+\newcommand{\iq}{\pad{\:}{\leadsto}}
+\newcommand{\mq}{\Longrightarrow}
+\newcommand{\retq}{\Rightarrow}
+\newcommand{\hq}{\pad{\:}{=}}
+\newcommand{\defq}{\mapsto}
+
+\newcommand{\refl}{\TC{refl}}
+
+
+
+
+%%%%%%%%%%%%% CATSTUFF
+
+\newlength{\Lwibrs}
+\newlength{\Lwobrs}
+\newsavebox{\Bwibrs}
+\newsavebox{\Bwobrs}
+\newcommand{\Db}[5]{%
+ \savebox{\Bwobrs}[\width][b]{$#5$}%
+ \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right#3$}%
+ \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
+ \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
+ \addtolength{\Lwibrs}{-\Lwobrs}%
+ \left#1\pad{\hspace*{-0.25\Lwibrs}}{\usebox{\Bwibrs}}\right#4}
+\newcommand{\LDb}[3]{%
+ \savebox{\Bwobrs}[\width][b]{$#3$}%
+ \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right.$}%
+ \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
+ \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
+ \addtolength{\Lwibrs}{-\Lwobrs}%
+ \left#1\hspace*{-0.4\Lwibrs}\usebox{\Bwibrs}\right.}
+\newcommand{\RDb}[3]{%
+ \savebox{\Bwobrs}[\width][b]{$#3$}%
+ \savebox{\Bwibrs}[\width][b]{$\left.\usebox{\Bwobrs}\right#1$}%
+ \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
+ \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
+ \addtolength{\Lwibrs}{-\Lwobrs}%
+ \left.\usebox{\Bwibrs}\hspace*{-0.4\Lwibrs}\right#2}
+\newcommand{\Sc}{\Db{[}{[}{]}{]}}
+\newcommand{\Mo}{\Db{|}{>}{<}{|}}
+\newcommand{\MoL}{\LDb{|}{>}}
+\newcommand{\MoR}{\RDb{<}{|}}
+
+\newcommand{\car}{\mbox{$-\!\triangleright$}}
+\newcommand{\io}[1]{\iota_{#1}}
+\newcommand{\cc}{\diamond}
+
+
+%%%%%%%%%%%%% FNS
+
+\newcommand{\Wk}{\Uparrow}
+
+%%%%%%%%%%%%% Transformation
+
+\newcommand{\Transform}[3]{\textsc{Trans}\:_{\Name{#1}}
+ \interp{#2}\:\mq\:#3}
+%\:[\:#2\:\Longrightarrow\:#3\:]}
+\newcommand{\Morphism}[2]{\textsc{Morphism}\:#1\:\Longrightarrow\:#2}
+\newcommand{\MI}[1]{\begin{array}{ll} #1 \end{array}\\}
+\newcommand{\MorphItem}[2]{& #1 \:\Longrightarrow\: #2}
+
+%%%%%%%%%%%%% Stuff
+
+% Motive and methods
+
+\newcommand{\motive}{\vP}
+\newcommand{\meth}[1]{\vm_{#1}}
+
+% Tuples
+\newcommand{\tuple}[1]{\langle#1\rangle}
+\newcommand{\Tuple}[1]{\mathsf{Tuple}}
+\newcommand{\proj}{\mathsf{proj}}
+\newcommand{\app}{\mathrm{+\!+}}
+
+% Commenting out
+\newcommand{\ig}[1]{[#1]}
+\newcommand{\rem}[1]{\{\!#1\!\}}
+\newcommand{\igc}[1]{[#1]}
+\newcommand{\remc}[1]{\{\!#1\!\}}
+
+
+\newcommand{\ind}{\hspace*{0.1cm}}
+
+% Content free type
+\newcommand{\CF}{\TC{CF}}
+\newcommand{\cf}{\DC{cf}}
+
+% Error token
+\newcommand{\error}{\DC{error}}
+\newcommand{\fail}{\perp}
+
+% Constructor stripping
+\newcommand{\conarg}[2]{#1!#2}
+
+\newcommand{\Vect}{\TC{Vect}}
+\newcommand{\VectM}{\TC{Vect^-}}
+\newcommand{\Vnil}{\DC{\epsilon}}
+\newcommand{\Vcons}{\DC{::}}
+
+\newcommand{\Vsnoc}{\DC{::}}
+
+\newcommand{\VnilM}{\DC{\epsilon^-}}
+\newcommand{\VconsM}{\DC{::^-}}
+
+\newcommand{\Vnilcase}{\VV{vNilCase}}
+\newcommand{\Vconscase}{\VV{vConsCase}}
+
+\newcommand{\DSigma}{\TC{Sigma}}
+\newcommand{\Exists}{\DC{Exists}}
+
+\newcommand{\ListPair}[2]{\sig{#1}{\List\:\vA}.#2 = \FN{length}\:#1}
+\newcommand{\lpNilDef}{\lpNil{\FN{refl}\:\Z}}
+\newcommand{\lpNil}[1]{(\nil\:\vA,#1)}
+\newcommand{\lpConsDef}[3]{\lpCons{#1}{(\FN{fst\:#2})}{\FN{resp}\:(\FN{snd}\:#2)}}
+\newcommand{\lpCons}[3]{(\cons\:#1\:#2,#3)}
+\newcommand{\lp}[2]{(#1, #2)}
+
+\newcommand{\VnilTop}{\DC{vNil}^\ast}
+\newcommand{\VconsTop}{\DC{vCons}^\ast}
+
+\newcommand{\VnilBot}{\DC{\epsilon}^-}
+\newcommand{\VconsBot}{\DC{::}^-}
+
+\newcommand{\VectTop}{\TC{Vect}^\ast}
+\newcommand{\VectBot}{\TC{Vect}^-}
+
+\newcommand{\VectDrop}{\FN{vectDropIdx}}
+\newcommand{\VectRebuild}{\FN{vectRebuild}}
+
+\newcommand{\Prop}{\TC{Prop}}
+\newcommand{\Set}{\TC{Set}}
+\newcommand{\CoqType}{\TC{Type}}
+
+\newcommand{\List}{\TC{List}}
+\newcommand{\nil}{\DC{nil}}
+\newcommand{\cons}{\DC{cons}}
+
+\newcommand{\Zip}{\TC{Tsil}}
+\newcommand{\zip}{\FN{tsil}}
+\newcommand{\zipcons}{\FN{tsilcons}}
+\newcommand{\snoc}{\DC{Snoc}}
+\newcommand{\lin}{\DC{Empty}}
+
+\newcommand{\BigInt}{\TC{BigInt}}
+\newcommand{\False}{\TC{False}}
+\newcommand{\Unit}{\TC{Unit}}
+\newcommand{\UnitI}{\DC{unit}}
+
+\newcommand{\genType}{\TC{X}}
+\newcommand{\genIndicesDec}{\tb\Hab\tB}
+\newcommand{\genIndices}{\tb}
+\newcommand{\genConArgsDec}[1]{\vec{\VV{a_#1}}\Hab\vec{\VV{A_#1}}}
+\newcommand{\genConArgs}[1]{\vec{\VV{a_#1}}}
+\newcommand{\genConIndicesDec}[1]{\vec{\VV{b_#1}}\Hab\vec{\VV{B_#1}}}
+\newcommand{\genConIndices}[1]{\vec{\VV{b_#1}}}
+\newcommand{\genCon}[1]{\DC{x}_#1}
+
+\newcommand{\genTypeTop}{\TC{X^\ast}}
+\newcommand{\genTypeBot}{\TC{X^-}}
+
+\newcommand{\genTypeDrop}{\FN{XDropIdx}}
+\newcommand{\genTypeRebuild}{\FN{XRebuild}}
+
+\newcommand{\HTerm}{\texttt{Term}}
+\newcommand{\Term}{\TC{Term}}
+\newcommand{\Var}{\DC{var}}
+\newcommand{\Lam}{\DC{lam}}
+\newcommand{\App}{\DC{app}}
+\newcommand{\TermM}{\TC{Term^-}}
+\newcommand{\VarM}{\DC{var^-}}
+\newcommand{\LamM}{\DC{lam^-}}
+\newcommand{\AppM}{\DC{app^-}}
+\newcommand{\Env}{\TC{Env}}
+\newcommand{\SType}{\TC{STy}}
+\newcommand{\farrow}{\Rightarrow}
+\newcommand{\lookup}{\FN{lookup}}
+
+% \newcommand{\source}{\Lang{TT}}
+\newcommand{\source}{\textbf{DT-Res}}
+\newcommand{\target}{\Lang{ExTT}}
+\newcommand{\runtime}{\Lang{RunTT}}
+
+\newcommand{\lt}{\TC{<}}
+\newcommand{\ltO}{\DC{ltO}}
+\newcommand{\ltS}{\DC{ltS}}
+
+\newcommand{\interp}[1]{\llbracket #1 \rrbracket}
+\newcommand{\inferrable}[2]{\FN{inferrable}(#1,#2)}
+\newcommand{\mkPat}{\FN{mkPat}}
+
+\newcommand{\FinM}{\TC{Fin^-}}
+\newcommand{\fzM}{\DC{f0^-}}
+\newcommand{\fsM}{\DC{fs^-}}
+
+\newcommand{\concat}{\mathrm{++}}
+
+%\newcommand{\bottom}{\perp}
+
+% Reductions
+
+\newcommand{\reduces}{\mapsto}
+\newcommand{\translation}{\Rightarrow}
+%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}
+%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}
+\newcommand{\reducesn}[1]{\reduces_{#1}}
+\newcommand{\reducesto}{\reduces^{*}}
+
+% Equality
+
+\newcommand{\Refl}{\DC{refl}}
+\newcommand{\leZ}{\DC{O_{\le}}}
+\newcommand{\leS}{\DC{S_{\le}}}
+
+% Random elimination things
+
+\newcommand{\lte}{\TC{\leq}}
+\newcommand{\lten}{\DC{leN}}
+\newcommand{\lteO}{\DC{leO}}
+\newcommand{\lteS}{\DC{leS}}
+
+\newcommand{\ltelim}{\Elim{\lt}}
+\newcommand{\leelim}{\Elim{\lte}}
+
+\newcommand{\dD}{\TC{D}}
+\newcommand{\delim}{\Elim{\TC{D}}}
+\newcommand{\drec}{\Rec{\TC{D}}}
+\newcommand{\dcase}{\Cases{\TC{D}}}
+\newcommand{\dview}{\View{\TC{D}}}
+\newcommand{\dmemo}{\Memo{\TC{D}}}
+\newcommand{\natrec}{\Rec{\Nat}}
+\newcommand{\natmemo}{\Memo{\Nat}}
+\newcommand{\natmemogen}{\Nat\textbf{-MemoGen}}
+\newcommand{\natelim}{\Elim{\Nat}}
+\newcommand{\boolcase}{\Cases{\Bool}}
+\newcommand{\vectrec}{\Rec{\Vect}}
+\newcommand{\vectelim}{\Elim{\Vect}}
+\newcommand{\listrec}{\Rec{\List}}
+\newcommand{\listelim}{\Elim{\List}}
+\newcommand{\finrec}{\Rec{\Fin}}
+\newcommand{\finelim}{\Elim{\Fin}}
+\newcommand{\natcase}{\Cases{\Nat}}
+\newcommand{\vectcase}{\Cases{\Vect}}
+\newcommand{\natdoublerec}{\Nat\textbf{-double-elim}}
+\newcommand{\eqelim}{=\textbf{-elim}}
+\newcommand{\falsecase}{\Cases{\False}}
+
+% Code
+\newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}
+
+% Quicksort
+
+\newcommand{\QSView}{\TC{QuickSort}}
+\newcommand{\qsempty}{\DC{empty}}
+\newcommand{\partition}{\DC{partition}}
+\newcommand{\qsview}{\FN{mkQuickSort}}
+
+% More gubbins
+
+\newcommand{\converts}{\simeq}
+\newcommand{\cumul}{\preceq}
+\newcommand{\whnf}{\Downarrow}
+\newcommand{\elem}{\in}
+\newcommand{\proves}{\vdash}
+\newcommand{\biimplies}{\Longleftrightarrow}
+
+\newcommand{\lc}{\lambda_{\mathsf{AC}}}
+\newcommand{\zed}{\mathbb{Z}}
+
+% Haskell keywords
+
+\newcommand{\hdata}{\mathtt{data}}
+\newcommand{\newtype}{\mathtt{newtype}}
+%\newcommand{\htype}{\mathtt{type}}
+
+\newcommand{\HTC}[1]{\mathtt{#1}}
+\newcommand{\HDC}[1]{\mathtt{#1}}
+
+% Nobby
+
+\newcommand{\Value}{\HTC{Value}}
+\newcommand{\VGamma}{\HTC{Env}}
+\newcommand{\Ctxt}{\HTC{Ctxt}}
+\newcommand{\Defs}{\HTC{Defs}}
+\newcommand{\ECtxt}{\HTC{ECtxt}}
+\newcommand{\TCtxt}{\HTC{TCtxt}}
+\newcommand{\VG}{\HDC{Env}}
+\newcommand{\Model}{\HTC{Model}}
+\newcommand{\Const}{\HTC{Const}}
+\newcommand{\Normal}{\HTC{Normal}}
+\newcommand{\Scope}{\HTC{Scope}}
+\newcommand{\Kripke}{\HTC{Kripke}}
+\newcommand{\Weakening}{\HTC{Weakening}}
+\newcommand{\Ready}{\HTC{Ready}}
+\newcommand{\Blocked}{\HTC{Blocked}}
+\newcommand{\Spine}{\HTC{Spine}}
+
+\newcommand{\BV}{\HDC{BV}}
+\newcommand{\BCon}{\HDC{BCon}}
+\newcommand{\BTyCon}{\HDC{BTyCon}}
+\newcommand{\RCon}{\HDC{RCon}}
+\newcommand{\RTyCon}{\HDC{RTyCon}}
+\newcommand{\BElim}{\HDC{BElim}}
+\newcommand{\DV}{\HDC{V}}
+\newcommand{\DP}{\HDC{P}}
+
+\newcommand{\MR}{\HDC{R}}
+\newcommand{\MB}{\HDC{B}}
+\newcommand{\DSc}{\HDC{Sc}}
+\newcommand{\DKr}{\HDC{Kr}}
+\newcommand{\DWk}{\HDC{Wk}}
+\newcommand{\DSnoc}{\HDC{;}}
+\newcommand{\DType}{\HDC{Type}}
+\newcommand{\DName}{\HDC{Name}}
+\newcommand{\DInt}{\HDC{Int}}
+\newcommand{\DString}{\HDC{String}}
+\newcommand{\DElim}{\HDC{Elim}}
+\newcommand{\Empty}{\HDC{\emptyset}}
+
+\newcommand{\ConCode}{\HTC{ConCode}}
+\newcommand{\ElimRule}{\HTC{ElimRule}}
+
+\newcommand{\DConst}{\HDC{Const}}
+\newcommand{\DCon}{\HDC{Con}}
+\newcommand{\DTyCon}{\HDC{TyCon}}
+\newcommand{\RConst}{\HDC{RConst}}
+\newcommand{\RLam}{\HDC{RLam}}
+\newcommand{\RPi}{\HDC{RPi}}
+\newcommand{\DLam}{\HDC{Lam}}
+\newcommand{\DLet}{\HDC{Let}}
+\newcommand{\DPi}{\HDC{Pi}}
+\newcommand{\DApp}{\HDC{App}}
+
+\newcommand{\TMaybe}{\HTC{Maybe}}
+\newcommand{\DNothing}{\HDC{Nothing}}
+\newcommand{\DJust}{\HDC{Just}}
+
+
+% G-machine and heap
+
+\newcommand{\PUSH}{\mathsf{PUSH}}
+\newcommand{\PUSHNAME}{\mathsf{PUSHNAME}}
+\newcommand{\POP}{\mathsf{DISCARD}}
+\newcommand{\PUSHFUN}{\mathsf{PUSHFUN}}
+\newcommand{\APPLY}{\mathsf{MKAP}}
+\newcommand{\EVAL}{\mathsf{EVAL}}
+\newcommand{\GCON}{\mathsf{MKCON}}
+\newcommand{\GTUP}{\mathsf{MKTUP}}
+\newcommand{\GTYPE}{\mathsf{MKTYPE}}
+\newcommand{\UPDATE}{\mathsf{UPDATE}}
+\newcommand{\RET}{\mathsf{RET}}
+\newcommand{\UNWIND}{\mathsf{UNWIND}}
+\newcommand{\CASEJUMP}{\mathsf{CASEJUMP}}
+\newcommand{\LABEL}{\mathsf{LABEL}}
+\newcommand{\MOVE}{\mathsf{MOVE}}
+\newcommand{\JUMP}{\mathsf{JUMP}}
+\newcommand{\SPLIT}{\mathsf{SPLIT}}
+\newcommand{\SQUEEZE}{\mathsf{SQUEEZE}}
+\newcommand{\JFUN}{\mathsf{JFUN}}
+\newcommand{\PROJ}{\mathsf{PROJ}}
+\newcommand{\ERROR}{\mathsf{ERROR}}
+\newcommand{\SLIDE}{\mathsf{SLIDE}}
+\newcommand{\ALLOC}{\mathsf{ALLOC}}
+
+\newcommand{\PUSHBIG}{\mathsf{PUSHBIG}}
+\newcommand{\PUSHBASIC}{\mathsf{PUSHBASIC}}
+\newcommand{\PUSHINT}{\mathsf{PUSHINT}}
+\newcommand{\PUSHBOOL}{\mathsf{PUSHBOOL}}
+\newcommand{\GET}{\mathsf{GET}}
+\newcommand{\MKINT}{\mathsf{MKINT}}
+\newcommand{\MKBOOL}{\mathsf{MKBOOL}}
+\newcommand{\ADD}{\mathsf{ADD}}
+\newcommand{\SUB}{\mathsf{SUB}}
+\newcommand{\MULT}{\mathsf{MULT}}
+\newcommand{\LT}{\mathsf{LT}}
+\newcommand{\EQ}{\mathsf{EQ}}
+\newcommand{\GT}{\mathsf{GT}}
+\newcommand{\JTRUE}{\mathsf{JTRUE}}
+
+\newcommand{\APP}{\mathsf{APP}}
+\newcommand{\FUN}{\mathsf{FUN}}
+\newcommand{\CON}{\mathsf{CON}}
+\newcommand{\TYCON}{\mathsf{TYCON}}
+\newcommand{\TUP}{\mathsf{TUP}}
+\newcommand{\TYPE}{\mathsf{TYPE}}
+\newcommand{\INT}{\mathsf{INT}}
+\newcommand{\BIGINT}{\mathsf{BIGINT}}
+\newcommand{\BOOL}{\mathsf{BOOL}}
+\newcommand{\HOLE}{\mathsf{HOLE}}
+
+% G machine translation scheme
+
+\newcommand{\sinterp}[1]{\mathcal{S}\interp{#1}}
+\newcommand{\sinterpm}[1]{\mathcal{S}\AR{\interp{#1}}}
+\newcommand{\einterp}[3]{\mathcal{E}\interp{#1}\:#2\:#3}
+\newcommand{\cinterp}[3]{\mathcal{C}\interp{#1}\:#2\:#3}
+\newcommand{\binterp}[3]{\mathcal{B}\interp{#1}\:#2\:#3}
+\newcommand{\rinterp}[3]{\mathcal{R}\interp{#1}\:#2\:#3}
+\newcommand{\iinterp}[3]{\mathcal{I}\interp{#1}\:#2\:#3}
+\newcommand{\len}[1]{\MO{length}(#1)}
+
+\newcommand{\casecomp}[2]{\mathcal{I}(#1,\left\{\ARc{#2}\right\})}
+\newcommand{\casecompA}[3]{\mathcal{I}(#1,\left\{\ARc{#2}\right\}[#3])}
+\newcommand{\ischeme}{\mathcal{I}}
+
+% tail call markup
+
+\newcommand{\tailcall}{\mathsf{tail}}
+
+% Trees
+
+\newcommand{\Tree}{\TC{Tree}}
+\newcommand{\Leaf}{\DC{Leaf}}
+\newcommand{\Node}{\DC{Node}}
+\newcommand{\treecase}{\Cases{\Tree}}
+
+% Languages
+
+\newcommand{\Coq}{\textsc{Coq}}
+\newcommand{\Lego}{\textsc{Lego}}
+\newcommand{\Oleg}{\textsc{Oleg}}
+\newcommand{\Alf}{\textsc{Alf}}
+\newcommand{\Epigram}{\textsc{Epigram}}
+\newcommand{\SystemF}{System $\mathcal{F}$}
+\newcommand{\Iswim}{\textsc{Iswim}}
+\newcommand{\Cynthia}{\textit{C$^Y$\hspace*{-0.1cm}NTHIA}}
+
+% Accessibility
+
+\newcommand{\Acc}{\TC{Acc}}
+\newcommand{\acc}{\DC{acc}}
+\newcommand{\qsAcc}{\TC{qsAcc}}
+\newcommand{\qsNil}{\DC{qsNil}}
+\newcommand{\qsCons}{\DC{qsCons}}
+\newcommand{\allQsAcc}{\FN{allQsAcc}}
+
+% Lazy shortcuts
+
+\newcommand{\naive}{na\"{\i}ve}
+\newcommand{\Naive}{Na\"{\i}ve}
+
+% Conor's bits
+
+\newcommand{\remem}[1]{\left|#1\right|}
+\newcommand{\idsb}{\MO{id}}
+\newcommand{\ang}[1]{\langle#1\rangle}
+
+\newcommand{\vePm}[1]{\vP #1 \vm_{\Vnil} #1 \vm_{\Vcons}}%
+\newcommand{\vcrhs}{\vm_{\Vcons}\:\vk\:\va\:\vv\:%
+ (\vectelim\:\vA\:\vk\:\vv\:\vePm{\:})}%
+
+\newcommand{\igV}[2]{#1^{\ig{#2}}}
+\newcommand{\remV}[2]{#1^{\rem{#2}}}
+
+% More gubbins
+
+\newcommand{\Between}{\TC{between}}
+\newcommand{\bZ}{\DC{bO}}
+\newcommand{\bZZS}{\DC{bOOs}}
+\newcommand{\bZSS}{\DC{b0ss}}
+\newcommand{\bSSS}{\DC{bsss}}
+\newcommand{\betelim}{\Elim{\Between}}
+\newcommand{\betrhs}[1]{\motive#1\meth{\bZ}#1\meth{\bZZS}#1\meth{\bZSS}#1\meth{\bSSS}}
+
+
+\newcommand{\valenv}{\TC{ValEnv}}
+\newcommand{\vempty}{\DC{empty}}
+\newcommand{\vextend}{\DC{extend}}
+
+\newcommand{\EpiVal}{\TC{Epigram}}
+\newcommand{\unsafeCoerce}{\HF{unsafeCoerce\mbox{\texttt{\#}}}}
+
+\newcommand{\qq}{\mbox{\texttt{"}}}
+\newcommand{\impossible}{\RW{Impossible}}
+
+\newcommand{\Real}{\mathbb{R}}
+
+\newcommand{\DoubleRec}{\TC{DoubleElim}}
+\newcommand{\DoubleOn}{\DC{Double_{\Z\vn}}}
+\newcommand{\DoubleSO}{\DC{Double_{\suc\Z}}}
+\newcommand{\DoubleSS}{\DC{Double_{\suc\suc}}}
+
+\newcommand{\doublerec}{\textbf{double-elim}}
+
+\newcommand{\set}{\TC{DList}}
+\newcommand{\setuser}{\TC{DListTop}}
+\newcommand{\setempty}{\emptyset}
+\newcommand{\setinsert}{\DC{insert}}
+
+
+%%%% Type systems
+
+\newcommand{\stlc}{\lambda\hspace*{-0.15cm}\to}
+\newcommand{\plc}{\lambda2}
+\newcommand{\dlc}{\lambda{}P}
+
+\newcommand{\EC}{\mathcal{E}}
+
+%%%% reductions
+
+\newcommand{\betared}{\iq\hspace*{-0.15cm}_{\beta}}
+\newcommand{\deltared}{\iq\hspace*{-0.15cm}_{\delta}}
+\newcommand{\gammared}{\iq\hspace*{-0.15cm}_{\gamma}}
+\newcommand{\etared}{\iq\hspace*{-0.15cm}_{\eta}}
+\newcommand{\iotared}{\iq\hspace*{-0.15cm}_{\iota}}
+\newcommand{\rhored}{\iq\hspace*{-0.15cm}_{\rho}}
+
+%%%% ExTT rules
+
+\newcommand{\exconverts}{\stackrel{\mathsf{Ex}}{\converts}}
+\newcommand{\excumul}{\stackrel{\mathsf{Ex}}{\cumul}}
+\newcommand{\exequiv}{\stackrel{\mathsf{Ex}}{\equiv}}
+\newcommand{\exreduces}{\stackrel{\mathsf{Ex}}\reduces}
+\newcommand{\exreducesto}{\stackrel{\mathsf{Ex}}{\reducesto}}
+\newcommand{\exreducesn}[1]{\exreduces_{#1}}
+
+\newcommand{\ttequiv}{\stackrel{\mathsf{TT}}{\equiv}}
+\newcommand{\ttreduces}{\stackrel{\mathsf{TT}}\reduces}
+\newcommand{\ttreducesn}[1]{\ttreduces_{#1}}
+
+%%% Type synthesis
+
+\newcommand{\hastype}{\Longrightarrow}
+\newcommand{\whnfs}{\twoheadrightarrow}
+\newcommand{\conv}{\converts}
+
+\newcommand{\exhastype}{\stackrel{\mathsf{Ex}}{\hastype}}
+\newcommand{\exwhnfs}{\stackrel{\mathsf{Ex}}{\whnfs}}
+\newcommand{\exconv}{\stackrel{\mathsf{Ex}}{\conv}}
+\newcommand{\exproves}{\stackrel{\mathsf{Ex}}{\proves}}
+
+\newcommand{\tthastype}{\stackrel{\mathsf{TT}}{\hastype}}
+\newcommand{\ttwhnfs}{\stackrel{\mathsf{TT}}{\whnfs}}
+\newcommand{\ttconv}{\stackrel{\mathsf{TT}}{\conv}}
+\newcommand{\ttproves}{\stackrel{\mathsf{TT}}{\proves}}
+
+%%% Lightning
+
+\newcommand{\light}[1]{\lightning^{#1}}
+\newcommand{\LHab}[1]{\pad{\;}{:^{#1}}}
+\newcommand{\llam}[3]{\lambda#1\pad{\!}{:}^{#2}#3}
+\newcommand{\lall}[3]{\forall#1\pad{\!}{:}^{#2}#3}
+\newcommand{\lapp}[3]{#1(#2)^{#3}}
+\newcommand{\larg}[2]{(#1)^{#2}}
+
+\newcommand{\RName}[1]{\hspace*{0.1in}\mathsf{#1}}
+
+%%% LOcal macros
+
+\newcommand{\ResState}{\TC{ResourceState}}
+\newcommand{\Locked}{\DC{Locked}}
+\newcommand{\ResHandle}{\TC{ResourceHandle}}
+\newcommand{\Res}{\DC{Resource}}
+\newcommand{\CLang}{\TC{CLang}}
+\newcommand{\CFLang}{\TC{CFLang}}
+\newcommand{\CFType}{\TC{CFType}}
+\newcommand{\CLType}{\TC{CType}}
+\newcommand{\RHandle}{\DC{RHandle}}
+\newcommand{\RType}{\DC{RType}}
+\newcommand{\RUnit}{\DC{RUnit}}
+\newcommand{\LOCK}{\DC{LOCK}}
+\newcommand{\UNLOCK}{\DC{UNLOCK}}
+\newcommand{\ACTION}{\DC{ACTION}}
+\newcommand{\FORK}{\DC{FORK}}
+
+\newcommand{\FSLang}{\TC{FSLang}}
+\newcommand{\OPEN}{\DC{OPEN}}
+\newcommand{\CLOSE}{\DC{CLOSE}}
+\newcommand{\READ}{\DC{READ}}
+\newcommand{\WRITE}{\DC{WRITE}}
+\newcommand{\PRINT}{\DC{PRINT}}
+\newcommand{\BIND}{\DC{BIND}}
+
+\newcommand{\FSType}{\TC{FSType}}
+\newcommand{\FHandle}{\DC{FHandle}}
+\newcommand{\FString}{\DC{FString}}
+\newcommand{\FUnit}{\DC{FUnit}}
+\newcommand{\ElemIs}{\TC{ElemIs}}
+\newcommand{\elemHd}{\TC{atHead}}
+\newcommand{\elemTl}{\TC{inTail}}
+
+\newcommand{\emptyEnv}{\DC{empty}}
+\newcommand{\extendEnv}{\DC{extend}}
+
+\newcommand{\usera}{\FN{Alice}}
+\newcommand{\userb}{\FN{Bob}}
+\newcommand{\userc}{\FN{Charlie}}
+
+\newcommand{\FAcc}{\TC{FAcc}}
+\newcommand{\UserA}{\DC{UserAcc}}
+\newcommand{\GroupA}{\DC{GroupAcc}}
+\newcommand{\GlobalA}{\DC{GlobalAcc}}
+
+\newcommand{\Perm}{\TC{Perm}}
+\newcommand{\Username}{\TC{Username}}
+\newcommand{\GroupData}{\TC{GroupData}}
+\newcommand{\File}{\TC{File}}
+\newcommand{\FS}{\DC{file}}
+\newcommand{\Filepath}{\TC{Filepath}}
+
+\newcommand{\Read}{\DC{Read}}
+\newcommand{\Write}{\DC{Write}}
+\newcommand{\Execute}{\DC{Execute}}
+
+\newcommand{\Purpose}{\TC{Mode}}
+\newcommand{\Reading}{\DC{Reading}}
+\newcommand{\Writing}{\DC{Writing}}
+
+\newcommand{\FileState}{\TC{FileState}}
+\newcommand{\FileHandle}{\TC{FileHandle}}
+\newcommand{\OpenH}{\DC{OpenH}}
+\newcommand{\ClosedH}{\DC{ClosedH}}
+\newcommand{\Handle}{\TC{Handle}}
+\newcommand{\Open}{\DC{Open}}
+\newcommand{\Closed}{\DC{Closed}}
+
+\newcommand{\UserIO}{\TC{UserIO}}
+\newcommand{\uio}{\DC{uio}}
+
+\newcommand{\CFS}{\TC{C_{fs}}}
+\newcommand{\RFS}{\FN{R_{fs}}}
+
+\newcommand{\String}{\TC{String}}
+
+% inline idris code
+
+\newcommand{\Tcon}[1]{\texttt{#1}}
+\newcommand{\Dcon}[1]{\texttt{#1}}
+\newcommand{\Fname}[1]{\texttt{#1}}
+\newcommand{\Vv}[1]{\texttt{#1}}
+\newcommand{\TyTy}{\texttt{\#}}
+
+\newcommand{\direct}[1]{\texttt{\%#1}}
+
+\newcommand{\Feature}[1]{\textbf{Remark:}}
+%\newcommand{\Remark}[1]{\textbf{Remark:}}
View
15 tutorial/miscellany.tex
@@ -0,0 +1,15 @@
+\section{Miscellany}
+
+Small things which don't quite fit elsewhere:
+
+\begin{itemize}
+\item Namespaces (other than modules)
+\item Literate programming
+\item Totality checking
+\item Foreign functions
+\end{itemize}
+
+\subsection{Comparison}
+
+How does \Idris{} compare with other dependently typed languages and proof
+assistants, such as Coq, Agda and Epigram?
View
144 tutorial/starting.tex
@@ -0,0 +1,144 @@
+\section{Getting Started}
+
+\subsection{Prerequisites}
+
+Before installing \Idris{}, you will need to make sure you have all of the necessary
+libraries and tools. You will need:
+
+\begin{itemize}
+\item A fairly recent Haskell platform. Version 2010.1.0.0.1 is currently
+sufficiently recent.
+\item The Boehm-Demers-Weiser garbage collector library. This is available in
+all major Linux distributions, or can be installed from source, available
+from \url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}. Installing from
+source is painless on MacOS.
+\item The GNU multiprecision arithmetic library, GMP, available from MacPorts and
+all major Linux distributions.
+\end{itemize}
+
+\subsection{Downloading and Installing}
+
+The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:
+
+\begin{SaveVerbatim}{install}
+
+cabal install idris
+
+\end{SaveVerbatim}
+\useverb{install}
+
+\noindent
+This will install the latest version released on Hackage\footnote{However version 0.9, which
+this tutorial describes, is not yet there, so don't do this. Finishing this tutorial is the
+last requirement before releasing it :-).}, along with any dependencies.
+If, however, you would like the most up
+to date development version, you can find it on GitHub at
+\url{https://github.com/edwinb/Idris-dev}.
+
+To check that installation has succeeded, and to write your first \Idris{}
+program, create a file called ``\texttt{hello.idr}'' containing the following
+text:
+
+\begin{SaveVerbatim}{hello}
+
+module main;
+
+main : IO();
+main = putStrLn "Hello world";
+
+\end{SaveVerbatim}
+\useverb{hello}
+
+\noindent
+If you are familiar with Haskell, it should be fairly clear what the program is doing
+and how it works, but if not, we will explain the details later.
+You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
+at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
+
+\begin{SaveVerbatim}{hello}
+
+$ idris hello.idr -o hello
+$ ./hello
+Hello world
+
+\end{SaveVerbatim}
+\useverb{hello}
+
+\noindent
+(Note that the \texttt{\$} indicates the shell prompt!)
+
+\subsection{The interactive environment}
+
+Entering \texttt{idris} at the shell prompt starts up the interactive
+environment. You should see something like the following:
+
+\begin{SaveVerbatim}{prompt1}
+
+$ idris
+ ____ __ _
+ / _/___/ /____(_)____
+ / // __ / ___/ / ___/ Version 0.9
+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
+ /___/\__,_/_/ /_/____/ Type :? for help
+
+Idris>
+
+\end{SaveVerbatim}
+%$
+
+\useverb{prompt1}
+
+This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
+as well as type checking expressions, theorem proving, compilation, editing
+and various other operations. \texttt{:?} gives a list of supported commands,
+as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
+\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
+the program is compiled to the executable \texttt{hello}.
+
+\begin{SaveVerbatim}{cmds}
+Idris version 0.9
+-----------------
+
+ Command Arguments Purpose
+
+ <expr> Evaluate an expression
+ :t <expr> Check the type of an expression
+ :r :reload Reload current file
+ :e :edit Edit current file using $EDITOR or $VISUAL
+ :m :metavars Show remaining proof obligations (metavariables)
+ :p :prove <name> Prove a metavariable
+ :a :addproof Add last proof to source file
+ :c :compile <filename> Compile to an executable <filename>
+ :exec :execute <filename> Compile to an executable <filename> and run
+ :? :h :help Display this help text
+ :q :quit Exit the Idris system
+\end{SaveVerbatim}
+\codefigs{cmds}{Interactive environment commands}
+
+
+\begin{SaveVerbatim}{run1}
+
+$ idris hello.idr
+ ____ __ _
+ / _/___/ /____(_)____
+ / // __ / ___/ / ___/ Version 0.9
+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
+ /___/\__,_/_/ /_/____/ Type :? for help
+
+Type checking ./hello.idr
+*hello> :t main
+main : IO ()
+*hello> :c hello
+*hello> :q
+Bye bye
+$ ./hello
+Hello world
+
+\end{SaveVerbatim}
+
+\codefig{run1}{Sample interactive run}
+
+Type checking a file, if successful, creates a bytecode version of the file (in this
+case \texttt{hello.ibc} to speed up loading in future. The bytecode is regenerated if
+the source file changes.
+
Please sign in to comment.
Something went wrong with that request. Please try again.