A Brown Paper Bag

Stop press. Thesis (uncensored version): .dvi and .ps.

In this brown paper bag is a gzipped tar of a directory which contains the nj-sml 0.93 source of my dodgy unstable LEGO version with gadgets for dependently typed programming. It's the version I actually use. And it's a mess.

I am making it available, but I am also promising not to support it. Bugs will not be fixed. Your proof scripts won't work on any other version of LEGO, past or future. You'll be very lucky if your old scripts work with this LEGO too.

You could probably use a library which might work some of the time.

I suppose I should describe the new features. I haven't got time to spill all the beans, but here's a sample session I cooked up.

The main reason this implementation is going in the bin is that it's all done wrong. I understand it much better now. I'm afraid it means goodbye to our old friends...

...and hello to this guy: he may be a bastard, but Janet Street-Porter probably has a point.

Conor's Work Page Last modified: Wed Jul 21 18:48:03 BST 1999