Two main windows are opened when ALF is started.
One window presents the theory and the other the scratch area. There are also two minor windows, one window showing the type of the current expression, and one window showing the constraints which must hold. This will be explained later.
The theory is a list of constants with their types and definition. The upper part of the theory window contains the imported theories, i.e. constants which reside in files which have been loaded by the system. Imported theories cannot be changed, they can only be changed by invoking the editor on the files they reside in. The other constants, the current theory, can be changed by first moving them to the scratch area.
The scratch area is a place where objects and types are being edited, so it contains incomplete objects and types. These objects can be built using the constants defined in the current theory and in the scratch area. When an object or type is completely built, it is moved to the theory window by the user. Below the scratch area there is a subwindow containing a set of constraints and a window showing the type of the selected expression.
Before we describe the menus which can be used in the two windows we have to explain how the mouse is used.