You can clone with
HTTPS or Subversion.
Abstract syntax with variable names.
While de Bruijn indices are The Right Thing to implement,
we opt for "pedestrian" syntax with variable names and
substitutions. This is extremely inefficient, but is much
easier to understand, as it is closer to theory.
Must go, but hunting down a bug in normalization
Better printout and other improvements
Syntax closer to Coq