Bj|rn von Sydow
- This research has been done within the ESPRIT Basic Research Action
``Types for Proofs and Programs''. It has been paid by NUTEK and Chalmers.
- Note that the type of
N is known now, which it was not the previous time we saw the menu.
- An unwanted feature of the present
version is that the constructors are reordered on the screen by this action.
This causes no harm, but is somewhat annoying.
- Note that it may be worthwhile to use postscript software to
adjust the bounding box.
- Contexts consists of list of variable declarations, i.e. a list of
variables together with their type. Every constant is defined in a context and
the variables in the context can be given a name by using a substitution.
This is in an experimental phase and only partly implemented.
- Tme implementation of Clear is based on the concept of
a local undo; details can be found in .
Wed Mar 20 13:05:14 MET 1996