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 := [ident0]{
ident1[:|:>]term1 ;
...
identn[:|:>]termn}.
The identifier ident is the name of the defined record and sort
is its type. The identifier ident0 is the name of its
constructor. The identifiers ident1, .., identn are the
names of its fields and term1, .., termn their respective
types. The alternative [:|:>] is ``:'' or ``:>''. If identi:>termi, then identi is
automatically declared as coercion from ident to the class of
termi. Remark that identi always verifies the uniform
inheritance condition. If the optional ``>'' before ident is
present, then ident0 (or the default name Build_ident
if ident0 is omitted) is automatically declared as a coercion
from the class of termn to ident (this may fail if the
uniform inheritance condition is not satisfied). Remark: The keyword Structure is a synonym of Record.