Attempt to make our markup respect the docbook specification(!), major changes

[helm.git] / helm / software / matita / help / C / sec_terms.xml

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index e9c1c054cc0201704491cbc5bc09cc56dc309842..fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -5,62 +5,67 @@
   <title>Syntax</title>
   <para>To describe syntax in this manual we use the following conventions:</para>
   <orderedlist>
   <title>Syntax</title>
   <para>To describe syntax in this manual we use the following conventions:</para>
   <orderedlist>

-   <listitem>Non terminal symbols are emphasized and have a link to their definition. E.g.: &term;</listitem>
-   <listitem>Terminal symbols are in bold. E.g.: <emphasis role="bold">theorem</emphasis></listitem>
-   <listitem>Optional sequences of elements are put in square brackets.
-    E.g.: [<emphasis role="bold">in</emphasis> &term;]</listitem>
-   <listitem>Alternatives are put in square brakets and they are separated
-    by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</listitem>
-   <listitem>Repetition of sequences of elements are given by putting the
+    <listitem><para>Non terminal symbols are emphasized and have a link to their
+       definition. E.g.: &term;</para></listitem>
+    <listitem><para>Terminal symbols are in bold. E.g.:
+       <emphasis role="bold">theorem</emphasis></para></listitem>
+    <listitem><para>Optional sequences of elements are put in square brackets.
+       E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
+    <listitem><para>Alternatives are put in square brakets and they are
+       separated by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</para></listitem>
+    <listitem><para>Repetition of sequences of elements are given by putting the

     first sequence in square brackets, that are followed by three dots.
     first sequence in square brackets, that are followed by three dots.

-    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
+    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>

   </orderedlist>
   <sect1 id="terms_and_co">
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
   </orderedlist>
   <sect1 id="terms_and_co">
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>

-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="id">&id;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="nat">&nat;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="uri">&uri;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
+  <para>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>id</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="id">&id;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>nat</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="nat">&nat;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>uri</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="uri">&uri;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+  </para>

   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>

-  <table>
+  <para>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Terms</title>

     <tgroup cols="4">
     <tgroup cols="4">

-     <thead />

     <tbody>
      <row>
       <entry id="term">&term;</entry>
     <tbody>
      <row>
       <entry id="term">&term;</entry>


@@ -144,9 +149,9 @@
    </tgroup>
   </table>
 
    </tgroup>
   </table>
 

-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Simple terms</title>

     <tgroup cols="4">
     <tgroup cols="4">

-     <thead />

     <tbody>
      <row>
       <entry id="sterm">&sterm;</entry>
     <tbody>
      <row>
       <entry id="sterm">&sterm;</entry>


@@ -241,9 +246,9 @@
    </tgroup>
   </table>
 
    </tgroup>
   </table>
 

-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Arguments</title>

     <tgroup cols="4">
     <tgroup cols="4">

-     <thead />

     <tbody>
      <row>
       <entry id="args">&args;</entry>
     <tbody>
      <row>
       <entry id="args">&args;</entry>


@@ -277,9 +282,9 @@
    </tgroup>
   </table>
 
    </tgroup>
   </table>
 

-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Miscellaneous arguments</title>

     <tgroup cols="4">
     <tgroup cols="4">

-     <thead />

     <tbody>
      <row>
       <entry id="args2">&args2;</entry>
     <tbody>
      <row>
       <entry id="args2">&args2;</entry>


@@ -297,9 +302,9 @@
    </tgroup>
   </table>
 
    </tgroup>
   </table>
 

-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Pattern matching</title>

     <tgroup cols="4">
     <tgroup cols="4">

-     <thead />

     <tbody>
      <row>
       <entry id="match_pattern">&match_pattern;</entry>
     <tbody>
      <row>
       <entry id="match_pattern">&match_pattern;</entry>


@@ -316,6 +321,7 @@
     </tbody>
    </tgroup>
   </table>
     </tbody>
    </tgroup>
   </table>

+  </para>

 
   </sect2>
   </sect1>
 
   </sect2>
   </sect1>


@@ -343,9 +349,30 @@
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
   </sect2>
   <sect2 id="inductive">
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
   </sect2>
   <sect2 id="inductive">

-    <title>[co]inductive &id; (of inductive types)</title>
+    <title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…
+[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]…
+</title>

     <titleabbrev>(co)inductive types declaration</titleabbrev>
     <titleabbrev>(co)inductive types declaration</titleabbrev>

-    <para> &TODO; </para>
+    <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
+    <para>Declares a family of two mutually inductive types
+     <command>i</command> and <command>i'</command> whose types are
+     <command>S</command> and <command>S'</command>, which must be convertible
+     to sorts.</para>
+    <para>The constructors <command>ki</command> of type <command>Ti</command>
+     and <command>ki'</command> of type <command>Ti'</command> are also
+     simultaneously declared. The declared types <command>i</command> and
+     <command>i'</command> may occur in the types of the constructors, but
+     only in strongly positive positions according to the rules of the
+     calculus.</para>
+    <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
+    <para>If the keyword <command>coinductive</command> is used, the declared
+     types are considered mutually coinductive.</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>i_ind</command>, <command>i_rec</command> and
+     <command>i_rect</command> according to the sort of their induction
+     predicate.</para> 

   </sect2>
   <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">:&gt;</emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:&gt;</emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
   </sect2>
   <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">:&gt;</emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:&gt;</emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>


@@ -360,8 +387,8 @@
     <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,
     <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
+     they are named <command>i_ind</command>, <command>i_rec</command> and
+     <command>i_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
      predicate.</para> 
     <para>For each field <command>fi</command> a record projection
      <command>fi</command> is also automatically generated if projection