\section{overview}

High level view of steps we've taken to implement this new version:

\begin{itemize}
\item Syntax tree for raw and well-typed terms
\item An evaluator for well-typed terms
\item The important bit: a simple type checker. No unification or
  inference.
\begin{itemize}
  \item It is extremely tempting to add implicit arguments and unification to the
        type checker. This is what I did in the first Idris prototype: I learned
        that it was a bad idea! Scope is a big problem.
\end{itemize}
\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).
\begin{itemize}
  \item Dealing with names: typechecking and evaluation in a context, managing de Bruijn
        indices becomes tricky. Instead: global names, local names during construction,
        and de Bruijn indices when done.
\end{itemize}
\item Unification, and incorporation into the tactic engine.
\begin{itemize}
  \item Note that this can introduce constraints on hole ordering. If we can't satisfy them,
        report an error.
\end{itemize}
\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and
      constructing derived tactics, from a high level syntax withe implicit arguments.
\item Advanced elaborations: using declarations, where clauses.
\item Adding primitive operators and a link to Epic~\cite{epic-tfp}.
\end{itemize}

For the high level language: we need nothing more than the core type theory,
and a way of putting stuff together. So we typecheck each pattern match clause
individually, in an appropriate context. There is no need for the core type
theory to have pattern matching.