DataSort includes elements representing all subsorts of Data, written as the lowercase spelling of the sort symbols. For any s in DataSort, the data operation the s is defined as the projection from Data to the subsort represented by s (the result being the argument when it is in the subsort, otherwise undefined). The data operations a s and an s are the same as the s, but intended for use when first referring to some given data (as in English). The data operation it abbreviates the datum, being defined only on 1tuples. |