\section{Introduction}

This paper documents a new implementation of \Idris{}~\cite{plpv11}, in which
I attempt to learn from the mistakes of the previous implementation and make
it nice and clean and solid. Maybe I'll keep it up to date as I write the
code.

The title is deliberately a reordering of the words in my thesis
title~\cite{brady-thesis}. Whereas that was about taking elaborated programs
in the core type theory of \Epigram{}~\cite{view-left} and compiling them
efficiently (i.e. making the language implementation practical) this paper is
about making the language itself practical. 

\subsection{Some Goals}

\begin{itemize}
\item Type checking dependent types~\cite{epireloaded,lambdapi} is just one component
 of a language. There is folklore about what to do to turn it into a language. This
 paper aims to help language implementers avoid working things out for themselves.
\item What's the difference between a theorem prover and a practical systems programming
 language? Not much...
\end{itemize}