Commands

The following commands are available in the toplevel environment:

Command	Description
def id = expression	binds the expression to id. The expression is type checked but not evaluated. Therefore this command is good to define abbreviations for types. If a $beta$ redex is found, it is marked.
rdef id = expression	binds the type checked and reduced expression to id. So this is the usual way to bind terms.
rstep expression	performs one evaluation step on expression and binds it to the default identifier it.
protocol e	outputs an execution protocol of the expression e.
equiv E1, E2	checks whether E1 and E2 are equal modulo full (!!!) $beta$-reduction.
use "filename"	loads a file into the interpreter
exit	exits the interpreter (CTRL+D on Linux has the same effect)
help	shows some information about the commands

To pass these commands to the interpreter, type ''<command>; <RETURN>''.

Furthermore there is the possibility to enter an expression at the toplevel. This is an abbreviation for ''rdef it = exp''. If you only type ''rstep'', then the interpreter tries to perform an evaluation step on the expression bound to it. Further abbreviations are ''def id = rstep'' and ''def id = rstep expression''. You can find a short example in section 6.

To change the behaviour of the interpreter use the switch command. The following alternatives are available:

Command	Description
switch pm o	changes the pretty printer to opaque output, i.e. hide definitions
switch pm t	switches the pretty printer to transparent output to expose definitions.
switch pm ows	changes the pretty printer to opaque output and tries in addition to synchronise the expressions with the environment. This check requires full $beta$-reduction and might therefore diverge in some cases.
switch pm terms	outputs only terms but no types.
switch pm types	outputs only types but no terms.
switch pm all	switches back to default to see both terms and terms.
switch tm s	switches the typing mode to s. Replace s by f, fw, cc, un, r, rg to switch to another mode. switch [no]sub enables or disables subtyping

Note: On switching the environment, it is always modified so that it only contains definitions which are well typed in the new mode.