14.2 Classes
14.2 Classes
A class with n parameters is any defined name with a type
(x1:A1)..(xn:An)s where s is a sort. Thus a class with
parameters is considered as a single class and not as a family of
classes. An object of a class C is any term of type (C t1
.. tn). In addition to these user-classes, we have two abstract
classes:
-
SORTCLASS, the class of sorts;
its objects are the terms whose type is a sort.
- FUNCLASS, the class of functions;
its objects are all the terms with a functional
type, i.e. of form (x:A)B.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.3.1.html at 8/10/98