Short term things to do:

* Allow holes in pattern matching definitions
* Need an easier way of updating a context with an input file
   (currently have to create a shell, then load, then create a new
   shell if you want to modify the context further)
* Improve error messages!
* Recursive functions shouldn't reduce at type level.
* Either better than Monad m? Define an Error type.
* Fix naming bug --- terms of form t1 -> t2 automatically give t1 the
  name X, which can clash. Particularly a problem in data type declarations.
* Current naive proof state representation is far too slow. Come up
  with something better.
* Keep track of level in proof state.
* Keep track of binding level in context, and check at point of use.
* Allow dump of global context to disk, for fast reloading.
* Syntax for equality.
* Elimination with a motive.
* Unit tests - at least check nat.tt, vect.tt, JM equality,
  primitives, simple staging, compiler.
* More readable high level language for function definition. Really
  just has to use tactic engine to translate simple case expressions into
  D-case calls.
* Separate API into several files for clarity.
* Allow call <fn args> _ in raw terms; i.e. allow the typechecker to
  spot recursive calls, rather than needing a tactic to do so.
* Finish compiler by:
  - Finding a method of exporting primitive types
  - Implement compilation of D-Case

Things which could be done to the library, in no particular order
(other than the order I thought of them in...):

* A higher level dependently typed language might be useful (e.g. like
  Coq's language). If not useful, at least fun :).
* Namespace management.
* Some useful error messages from the Parsec parsers would be nice.
* Proper type universes, of some form.
* Generate DRec and DNoConfusion as well as DElim/DCase.
* Build in Sigma types? (At least a nicer syntax?)
* Infix operators, especially = would be nice.

Tactics:

* Injectivity.
* Discriminate.
* Inversion.