+ <sect2 id="record">
+ <title><emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
+ <titleabbrev>record</titleabbrev>
+ <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
+ <para>Declares a new record family <command>id</command> parameterized over
+ <command>x,y,z</command>.</para>
+ <para><command>S</command> is the type of the record
+ and it must be convertible to a sort.</para>
+ <para>Each field <command>fi</command> is declared by giving its type
+ <command>Ti</command>. A record without any field is admitted.</para>
+ <para>Elimination principles for the record are automatically generated
+ by Matita, if allowed by the typing rules of the calculus according to
+ the sort <command>S</command>. If generated,
+ they are named <command>id_ind</command>, <command>id_rec</command> and
+ <command>id_rect</command> according to the sort of their induction
+ predicate.</para>
+ <para>For each field <command>fi</command> a record projection
+ <command>fi</command> is also automatically generated if projection
+ is allowed by the typing rules of the calculus according to the
+ sort <command>S</command>, the type <command>T1</command> and
+ the definability of depending record projections.</para>
+ <para>If the type of a field is declared with <command>:></command>,
+ the corresponding record projection becomes an implicit coercion.
+ This is just syntactic sugar and it has the same effect of declaring the
+ record projection as a coercion later on.</para>
+ </sect2>