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).

Set

Create a new a set or a family of sets.

Type

Create an explicitly defined constant denoting a type.

Context

Create a named context .

Substitution

Create a named substitution. Not implemented yet.