next up previous contents
Next: The Construct-menu Up: The scratch area Previous: The File-menu

The Define-menu

When you start to build something in the scratch area you first have to tell what kind of thing you are going to build and then giving it a name. This is done with selections from this menu.

Explicit Constant
Create an explicitly defined constant. This has a definiendum (a name, a left hand side), a definiens (a right hand side), a type and a context. After giving the name the other parts are filled in by the user by replacing place-holders (question marks) with other expressions.
Implicit Constant
Create a new implicitly defined constant. This is a constant which is defined by pattern-matching and possibly recursively defined. After giving it a name, you tell what type it should have (by incrementally editing placeholders).
Create a new a set or a family of sets.
Create an explicitly defined constant denoting a type.
Create a named context gif.
Create a named substitution. Not implemented yet.

Bj|rn von Sydow
Wed Mar 20 13:05:14 MET 1996