implementing constructive type theory TT0

[dr.mt...@gmail.com]

This is ground I've done before but this time with more depth and care.

Building it in the Logic Lab has been fascinating if challenging.  The

derivation rules attached take a v. big typechecking load.

run time: 1.73388671875 secs
typechecked in 2747839 inferences

And that is with embedded type declarations - all for a file of 207 lines!

Without maxinferences reconfigured from the default 10^6; this will not

load.  I'll look at streamlining the type theory for TT0 syntax.

While doing this work and developing the LogicLab I uncovered 2 bugs in the

Shen kernel which I have corrected.   I'll issue this as S41.

Mark