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