14.3 Coercions

A name f can be declared as a coercion between a source user-class C with n parameters and a target class D if one of these conditions holds:

We then write f:C >-> D. The restriction on the type of coercions is called the uniform inheritance condition. Remark that the abstract classes FUNCLASS and SORTCLASS cannot be source classes.

To coerce an object t:(C t1..tn) of C towards D, we have to apply the coercion f to it; the obtained term (f t1..tn t) is then an object of D.