In some cases deeper insight in the cause of a semantic error may be acquired from stepwise inspection of types of program constructs. This can be accomplished by the verify-command, which causes the checker to run in trace-mood. Its behaviour is analogous to the trace-mood, with the exception that the types of the program constructs are displayed rather than their value.