TYPESUBST : MEXPR

TYPESUBST is a top-level command.
Substitute for a type variable in one line to infer another line.
The type variable must not appear in any hypothesis.
The command format for TYPESUBST is:

 <n>TYPESUBST    D    P     A       B 
"LINE" "LINE" "TYPESYM" "TYPESYM"


The arguments have the following meaning:
D : Line before Type Substitution
P : Line after Type Substitution
A : Type Variable
B : Type to Substitute for Type Variable

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage