CAST ::= cast TERM SORT
A cast term is written:
T as s
It is well-sorted if the term T is well-sorted for a supersort s' of s. It expands to an application of the pre-declared operation symbol for projecting from s' to s.
Term formation is also extended by letting a well-sorted term of a subsort s be regarded as a well-sorted term of a supersort s' as well, which provides implicit embedding. It expands to the explicit application of the pre-declared operation symbol for embedding s into s'. (There are no implicit projections.) Also a sorted-term T:s' expands to an explicit application of an embedding, provided that the apparent sort s of the component term T is a subsort of the specified sort s'.