\documentclass{article}

\usepackage{fullpage}
\usepackage{palatino}
\usepackage{url}
\usepackage{fancyvrb}

\input{macros.ltx}
\input{library.ltx}

\newcommand{\Idris}{\textsc{Idris}}

\title{Programming in \Idris{}: a tutorial}
\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}

\begin{document}

\maketitle

%\tableofcontents

\input{intro}
\input{starting}
\input{typesfuns}
\input{classes}

%Planned sections

\section{Example: The Well-Typed Interpreter}
\section{Views}
\section{Theorem Proving}
\section{Provisional Definitions}
\section{Syntax Extensions}
%\section{Example: A verified binary adder}

\input{miscellany}

\bibliographystyle{abbrv}
\bibliography{literature.bib}

\end{document}