20010419

  The representation of contexts has changed to a linked list.  This is
mostly to support proof search, in which the contexts should be shared.
  I'm rewriting the proof search stuff along the lines of

Dowek, Gilles.  A complete proof synthesis method for the cube of type
  systems.  Journal of Logic and Computation, 3(3):287-315, June 1993.

20001121

  The representation of bound variables has changed.  Previously I was just
using the named representation.  Now, a variable is represented by a Var
object, which contains the variable's name.  Every occurrance of that
variable in a Term is represented by a reference to the corresponding
Var object.  (Although I'm starting to think that de Bruijn indices
would be easier to use.)

  I'm now using the JavaCup parser generator, and JLex scanner generator,
from some people at Princeton University:

http://www.cs.princeton.edu/~appel/modern/java/CUP/index.html

This adds a bit of complication, but means that I don't have to keep
modifying a hand-written recursive-descent parser.  This should make
the grammar _much_ easier to read and modify.

  There are dependent record types now; but no subtyping yet.
ML-style datatypes can be represented using some syntactic sugar:

data Bool = True | False

can be represented by the type

bool = pi c:star . { true:c; false:c } -> c;

  This is a compromise between the Church encodings (which don't add
new axioms, but are hard to read) and datatypes in Coq or Lego (which have
names, but require adding new axioms each time a datatype is declared.)
It still looks kind of ugly, though; it may be worth adding sum types.
  Note that adding new datatypes in this scheme doesn't require asserting
new axioms, as it does in Lego.  (Instead of having an induction axiom
for each type, I'm planning on just using induction on the natural
numbers, which should be equivalent.)

  I'm not sure what to name it.

