14.8 Classes as Records

We allow the definition of Structures with Inheritance (or classes as records) by extending the existing Record macro (see section 2.1). Its new syntax is:

Record ident [ params ] : sort := ident₀ {

ident₁ [:|:>] term₁ ;

...

ident_n [:|:>] term_n }.

The identifier ident is the name of the defined record and sort is its type. The identifier ident₀ is the name of its constructor. The identifiers ident₁, .., ident_n are the names of its fields and term₁, .., term_n their respective types. The alternative [:|:>] is ``:'' or ``:>''. If ident_i:>term_i, then ident_i is automatically declared as coercion from ident to the class of term_i. Remark that ident_i always verifies the uniform inheritance condition. The keyword Structure is a synonym of Record.

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