Next: The Construct-menu
Up: The scratch area
Previous: The File-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
Create a named substitution. Not implemented yet.
Bj|rn von Sydow
Wed Mar 20 13:05:14 MET 1996