The Construct-menu

When the current selection is a placeholder it is possible to replace the placeholder with different new incomplete expressions. Depending on where the placeholder is, diffferent replacements can be made. These are the alternatives:

[x]?

In the case that the expected type of a placeholder is a function or a place holder then it is possible to replace it by an abstraction.

[x...]?

This replaces the placeholder with a repeated abstraction.

case ?

Replaces the placeholder with a case-expression. This can only be done if the placeholder is the righthand side of an equation of an implicitly defined constant or is the righthand side of a branch of another case expression. These restrictions will be removed.

Make a pattern

If the current selection is a typing of an implicitly defined constant or a variable in the lefthand side of an implicitly defined constant then this command will create new defining equations for this constant. This command is also used to create a pattern in a case-expression.

Set

Replaces the current placeholder with the expression .

Prop

Replaces the current placeholder with the expression .

(?)?

Replaces the current placeholder with the expression , i.e. a non-dependent function type.

(x : ?)?

Asks for a variable name x and replaces the current placeholder with an expression which is a template for a dependent function type.

Make a constructor

If the current selection is a typing of a set or a family of sets, then this command will ask the user to input the name of a new constructor for this set. As an example, if the current selection is

then the user is asked to give the name of a constructor of .

[]

Creates an empty context. Not implemented yet.

... + ?

Adds a context to a context. Not implemented yet.

x : ?

extends a context with the declaration of a new variable (which is prompted for).

{}

Creates an empty substitution. Not implemented yet.

x := ?

Makes a substitution. Not implemented yet.