The Subtyping Relation between Types

A  B

As indicated in Subtype Relation, the standard set of primitive operators has not included a notation for the two-place relation of subtyping between two types. In advance of it adoption for normal development, some users have forged ahead with its incorporation, though tactic support is still not adequate for the typical user. The operator is A  B. It differs from A  B in its well-formedness conditions. While A  B is a well formed proposition only when it is true, and so is useless as the antecedent of an implication, A  B is a well formed proposition so long as A and B are type expressions, independently of whether A really is a subtype of B. (On the other hand, A  B is well formed if A denotes the empty type no matter whether B denotes a type.)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html