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.
