CALS tables enriched to make (crappy) docbook stylesheets happy.

[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 93dd12bef734e4fde0d5920a913935b6850529c6..5e29eb41eec2fce914c6d8b73119753482f63198 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -2,12 +2,25 @@
 <!-- =========== Terms, declarations and definitions ============ -->
 
 <chapter id="sec_terms">
-  <title>Terms, axioms, definitions, declarations and proofs</title>
-
-  <sect1 id="terms">
-  <title>Terms</title>
+  <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
+    first sequence in square brackets, that are followed by three dots.
+    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
+  </orderedlist>
+  <sect1 id="terms_and_co">
+  <title>Terms &amp; co.</title>
+  <sect2 id="lexical">
+  <title>Lexical conventions</title>
   <table>
-    <tgroup>
+    <tgroup cols="4">
      <thead />
     <tbody>
      <row>
@@ -19,7 +32,7 @@
    </tgroup>
   </table>
   <table>
-    <tgroup>
+    <tgroup cols="4">
      <thead />
     <tbody>
      <row>
@@ -31,7 +44,7 @@
    </tgroup>
   </table>
   <table>
-    <tgroup>
+    <tgroup cols="4">
      <thead />
     <tbody>
      <row>
@@ -42,75 +55,153 @@
     </tbody>
    </tgroup>
   </table>
+  </sect2>
+  <sect2 id="terms">
+  <title>Terms</title>
   <table>
-    <tgroup>
+    <tgroup cols="4">
      <thead />
     <tbody>
      <row>
       <entry id="term">&term;</entry>
       <entry>::=</entry>
-      <entry>&id;</entry>
-      <entry>identifier</entry>
+      <entry>&sterm;</entry>
+      <entry>simple or delimited term</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry>&uri;</entry>
-      <entry>a qualified reference</entry>
+      <entry>&term; &term;</entry>
+      <entry>application</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">Prop</emphasis></entry>
-      <entry>the impredicative sort of propositions</entry>
+      <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+      <entry>λ-abstraction</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">Set</emphasis></entry>
-      <entry>the impredicate sort of datatypes</entry>
+      <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+      <entry>dependent product meant to define a datatype</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">Type</emphasis></entry>
-      <entry>one predicatie sort of datatypes</entry>
+      <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
+      <entry>dependent product meant to define a proposition</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry>&term; &term;</entry>
-      <entry>application</entry>
+      <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
+      <entry>non-dependent product (logical implication or function space)</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">λ</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
-      <entry>λ-abstraction</entry>
+      <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
+      <entry>local definition</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">Π</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
-      <entry>dependent product meant to define a datatype</entry>
+      <entry><emphasis role="bold">let</emphasis>
+      [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
+      &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
+      [<emphasis role="bold">:</emphasis> &term;]
+      <emphasis role="bold">≝</emphasis> &term;
+      </entry>
+      <entry>(co)recursive definitions</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry/>
+      <entry>
+      [<emphasis role="bold">and</emphasis>
+      [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
+      [<emphasis role="bold">:</emphasis> &term;]
+      <emphasis role="bold">≝</emphasis> &term;]…
+      </entry>
+      <entry/>
+     </row>
+     <row>
+      <entry/>
+      <entry/>
+      <entry>
+      <emphasis role="bold">in</emphasis> &term;
+      </entry>
+      <entry/>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">∀</emphasis>&id;[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">.</emphasis>&term;</entry>
-      <entry>dependent product meant to define a proposition</entry>
+      <entry>…</entry>
+      <entry>user provided notation</entry>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+
+  <table>
+    <tgroup cols="4">
+     <thead />
+    <tbody>
+     <row>
+      <entry id="sterm">&sterm;</entry>
+      <entry>::=</entry>
+      <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
+      <entry/>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
-      <entry>non-dependent product (logical implication or function space)</entry>
+      <entry>&id;[<emphasis role="bold">\subst[</emphasis>
+       &id;<emphasis role="bold">≔</emphasis>&term;
+       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
+       <emphasis role="bold">]</emphasis>]
+      </entry>
+      <entry>identifier with optional explicit named substitution</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
-      <entry>local definition</entry>
+      <entry>&uri;</entry>
+      <entry>a qualified reference</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">Prop</emphasis></entry>
+      <entry>the impredicative sort of propositions</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">Set</emphasis></entry>
+      <entry>the impredicate sort of datatypes</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">Type</emphasis></entry>
+      <entry>one predicative sort of datatypes</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">?</emphasis></entry>
+      <entry>implicit argument</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">?n</emphasis>
+      [<emphasis role="bold">[</emphasis>
+      [<emphasis role="bold">_</emphasis>|&term;]…
+      <emphasis role="bold">]</emphasis>]</entry>
+      <entry>metavariable</entry>
      </row>
      <row>
       <entry/>
@@ -127,41 +218,59 @@
       <entry/>
       <entry>
        <emphasis role="bold">[</emphasis> 
-       &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+       &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
          [
          <emphasis role="bold">|</emphasis>
-         &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+         &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
          ]…<emphasis role="bold">]</emphasis> </entry>
       <entry/>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">let</emphasis>
-      [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
-      &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
-      [<emphasis role="bold">:</emphasis> &term;]
-      <emphasis role="bold">≝</emphasis> &term;
-      </entry>
-      <entry>(co)recursive definitions</entry>
+      <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
+      <entry>cast</entry>
      </row>
      <row>
       <entry/>
-      <entry/>
+      <entry>|</entry>
+      <entry>…</entry>
+      <entry>user provided notation at precedence 90</entry>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+
+  <table>
+    <tgroup cols="4">
+     <thead />
+    <tbody>
+     <row>
+      <entry id="args">&args;</entry>
+      <entry>::=</entry>
       <entry>
-      [<emphasis role="bold">and</emphasis>
-      &id; [&id;]… [<emphasis role="bold">on</emphasis> &nat;]
-      [<emphasis role="bold">:</emphasis> &term;]
-      <emphasis role="bold">≝</emphasis> &term;]…
+       <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
       </entry>
-      <entry/>
+      <entry>ignored argument</entry>
      </row>
      <row>
       <entry/>
-      <entry/>
+      <entry>|</entry>
       <entry>
-      <emphasis role="bold">in</emphasis> &term;
+       <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
       </entry>
+      <entry>ignored argument</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
+      <entry></entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
       <entry/>
      </row>
     </tbody>
@@ -169,11 +278,11 @@
   </table>
 
   <table>
-    <tgroup>
+    <tgroup cols="4">
      <thead />
     <tbody>
      <row>
-      <entry id="term_pattern">&term_pattern;</entry>
+      <entry id="match_pattern">&match_pattern;</entry>
       <entry>::=</entry>
       <entry>&id;</entry>
       <entry>0-ary constructor</entry>
@@ -187,16 +296,19 @@
     </tbody>
    </tgroup>
   </table>
+
+  </sect2>
   </sect1>
 
-  <sect1 id="axiom">
+  <sect1 id="axiom_definition_declaration">
+   <title>Definitions and declarations</title>
+   <sect2 id="axiom">
     <title>axiom &id;: &term;</title>
     <titleabbrev>axiom</titleabbrev>
     <para><userinput>axiom H: P</userinput></para>
     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
-  </sect1>
-
-  <sect1 id="definition">
+  </sect2>
+  <sect2 id="definition">
     <title>definition &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>definition</titleabbrev>
     <para><userinput>definition f: T ≝ t</userinput></para>
@@ -209,12 +321,12 @@
      given. In this case Matita enters in interactive mode and
      <command>f</command> must be defined by means of tactics.</para>
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
-  </sect1>
-
-  <sect1 id="inductive">
+  </sect2>
+  <sect2 id="inductive">
     <title>[co]inductive &id; (of inductive types)</title>
     <titleabbrev>(co)inductive types declaration</titleabbrev>
     <para> &TODO; </para>
+  </sect2>
   </sect1>
 
   <sect1 id="proofs">