git.iko.soy/Idris-dev
on dcba960 help sign in
Idris-dev/tutorial/idris-tutorial.tex
38 lines 606 B history raw
1\documentclass{article}
3\usepackage{fullpage}
4\usepackage{palatino}
5\usepackage{url}
6\usepackage{fancyvrb}
8\input{macros.ltx}
9\input{library.ltx}
11\newcommand{\Idris}{\textsc{Idris}}
13\title{Programming in \Idris{}: a tutorial}
14\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
16\begin{document}
18\maketitle
20\tableofcontents
22\input{intro}
23\input{starting}
24\input{typesfuns}
25\input{classes}
26\input{modules}
27\input{interp}
28\input{views}
29\input{theorems}
30\input{provisional}
31\input{syntax}
32\input{miscellany}
33\input{conclusions}
35\bibliographystyle{abbrv}
36\bibliography{literature.bib}
38\end{document}