14.4 Inheritance Graph
14.4 Inheritance Graph
Coercions form an inheritance graph with classes as nodes. We call
path coercion an ordered list of coercions between two nodes of
the graph. A class C is said to be a subclass of D if there is a
coercion path in the graph from C to D; we also say that C
inherits from D. Our mechanism supports multiple inheritance since a
class may inherit from several classes, contrary to simple inheritance
where a class inherits from at most one class. However there must be
at most one path between two classes. If this is not the case, only
the oldest one is valid and the others are ignored. So the order
of declaration of coercions is important.
We extend notations for coercions to path coercions. For instance
[f1;..;fk]:C >-> D is the coercion path composed
by the coercions f1..fk. The application of a path-coercion to a
term consists of the successive application of its coercions.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.3.3.html at 8/10/98