git.iko.soy/Idris-dev
on dd03041 help sign in
Idris-dev/tutorial/idris-tutorial.tex
41 lines 705 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}
27%Planned sections
29\section{Example: The Well-Typed Interpreter}
30\section{Views}
31\section{Theorem Proving}
32\section{Provisional Definitions}
33\section{Syntax Extensions}
34%\section{Example: A verified binary adder}
36\input{miscellany}
38\bibliographystyle{abbrv}
39\bibliography{literature.bib}
41\end{document}