14.1 General Presentation

This section describes the inheritance mechanism of Coq. In Coq with inheritance, we are not interested in adding any expressive power to our theory, but only convenience. Given a term, possibly not typable, we are interested in the problem of determining if it can be well typed modulo insertion of appropriate coercions. We allow to write:

(f a) where f:(x:A)B and a:A' when A' can be seen in some sense as a subtype of A.
x:A when A is not a type, but can be seen in a certain sense as a type: set, group, category etc.
(f a) when f is not a function, but can be seen in a certain sense as a function: bijection, functor, any structure morphism etc.

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.3.0.html at 8/10/98