From 9c67c1566df112f5c35d752361bd02b6a3742993 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 25 May 2006 17:13:58 +0000
Subject: [PATCH] More documentation.

---
 matita/help/C/matita.xml      |   7 +
 matita/help/C/sec_tactics.xml |  50 +++----
 matita/help/C/sec_terms.xml   | 270 ++++++++++++++++++++++++----------
 3 files changed, 222 insertions(+), 105 deletions(-)

diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index 05e0a8212..357727961 100644
--- a/matita/help/C/matita.xml
+++ b/matita/help/C/matita.xml
@@ -17,6 +17,13 @@
   <!ENTITY TODO "<emphasis>TODO</emphasis>">
   <!ENTITY MYSQL "<application> <ulink type='http'
       url='http://www.mysql.com'>MySQL</ulink> </application>">
+
+  <!-- Entities for BNF -->
+  <!ENTITY id "<emphasis><link linkend='id'>id</link></emphasis>">
+  <!ENTITY uri "<emphasis><link linkend='uri'>uri</link></emphasis>">
+  <!ENTITY nat "<emphasis><link linkend='nat'>nat</link></emphasis>">
+  <!ENTITY term "<emphasis><link linkend='term'>term</link></emphasis>">
+  <!ENTITY term_pattern "<emphasis><link linkend='term_pattern'>term_pattern</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 4bba23eb6..fb695879f 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -4,7 +4,7 @@
  <title>Tactics</title>
 
   <sect1 id="tac_absurd">
-    <title>absurd &lt;term&gt;</title>
+    <title>absurd &term;</title>
     <titleabbrev>absurd</titleabbrev>
     <para><userinput>absurd P</userinput></para>
      <para>
@@ -33,7 +33,7 @@
      </para>
   </sect1>
   <sect1 id="tac_apply">
-    <title>apply &lt;term&gt;</title>
+    <title>apply &term;</title>
     <titleabbrev>apply</titleabbrev>
     <para><userinput>apply t</userinput></para>
     <para>
@@ -96,7 +96,7 @@
     </para>
   </sect1>
   <sect1 id="tac_auto">
-    <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
+    <title>auto [depth=&nat;] [width=&nat;] [paramodulation] [full]</title>
     <titleabbrev>auto</titleabbrev>
     <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
     <para>
@@ -130,7 +130,7 @@
     </para>
   </sect1>
   <sect1 id="tac_clear">
-    <title>clear &lt;id&gt;</title>
+    <title>clear &id;</title>
     <titleabbrev>clear</titleabbrev>
     <para><userinput>clear H</userinput></para>
     <para>
@@ -159,7 +159,7 @@
     </para>
   </sect1>
   <sect1 id="tac_clearbody">
-    <title>clearbody &lt;id&gt;</title>
+    <title>clearbody &id;</title>
     <titleabbrev>clearbody</titleabbrev>
     <para><userinput>clearbody H</userinput></para>
     <para>
@@ -188,7 +188,7 @@
     </para>
   </sect1>
   <sect1 id="tac_change">
-    <title>change &lt;pattern&gt; with &lt;term&gt;</title>
+    <title>change &lt;pattern&gt; with &term;</title>
     <titleabbrev>change</titleabbrev>
     <para><userinput>change patt with t</userinput></para>
     <para>
@@ -220,7 +220,7 @@
     </para>
   </sect1>
   <sect1 id="tac_constructor">
-    <title>constructor &lt;int&gt;</title>
+    <title>constructor &nat;</title>
     <titleabbrev>constructor</titleabbrev>
     <para><userinput>constructor n</userinput></para>
     <para>
@@ -281,7 +281,7 @@
     </para>
   </sect1>
   <sect1 id="tac_cut">
-    <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
+    <title>cut &term; [as &id;]</title>
     <titleabbrev>cut</titleabbrev>
     <para><userinput>cut P as H</userinput></para>
     <para>
@@ -312,7 +312,7 @@
     </para>
   </sect1>
   <sect1 id="tac_decompose">
-    <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
+    <title>decompose &id; [&id;]… [&lt;intros_spec&gt;]</title>
     <titleabbrev>decompose</titleabbrev>
     <para><userinput>decompose ???</userinput></para>
     <para>
@@ -339,7 +339,7 @@
     </para>
   </sect1>
   <sect1 id="tac_discriminate">
-    <title>discriminate &lt;term&gt;</title>
+    <title>discriminate &term;</title>
     <titleabbrev>discriminate</titleabbrev>
     <para><userinput>discriminate p</userinput></para>
     <para>
@@ -368,7 +368,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_elim">
-    <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
+    <title>elim &term; [using &term;] [&lt;intros_spec&gt;]</title>
     <titleabbrev>elim</titleabbrev>
     <para><userinput>elim t using th hyps</userinput></para>
     <para>
@@ -405,7 +405,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_elimType">
-    <title>elimType &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
+    <title>elimType &term; [using &term;] [&lt;intros_spec&gt;]</title>
     <titleabbrev>elimType</titleabbrev>
     <para><userinput>elimType T using th hyps</userinput></para>
     <para>
@@ -432,7 +432,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_exact">
-    <title>exact &lt;term&gt;</title>
+    <title>exact &term;</title>
     <titleabbrev>exact</titleabbrev>
     <para><userinput>exact p</userinput></para>
     <para>
@@ -518,7 +518,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_fold">
-    <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
+    <title>fold &lt;reduction_kind&gt; &term; &lt;pattern&gt;</title>
     <titleabbrev>fold</titleabbrev>
     <para><userinput>fold red t patt</userinput></para>
     <para>
@@ -580,7 +580,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_fwd">
-    <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
+    <title>fwd &id; [&lt;ident list&gt;]</title>
     <titleabbrev>fwd</titleabbrev>
     <para><userinput>fwd ...TODO</userinput></para>
     <para>
@@ -607,7 +607,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_generalize">
-    <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
+    <title>generalize &lt;pattern&gt; [as &id;]</title>
     <titleabbrev>generalize</titleabbrev>
     <para><userinput>generalize patt as H</userinput></para>
     <para>
@@ -670,7 +670,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_injection">
-    <title>injection &lt;term&gt;</title>
+    <title>injection &term;</title>
     <titleabbrev>injection</titleabbrev>
     <para><userinput>injection p</userinput></para>
     <para>
@@ -701,7 +701,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_intro">
-    <title>intro [&lt;ident&gt;]</title>
+    <title>intro [&id;]</title>
     <titleabbrev>intro</titleabbrev>
     <para><userinput>intro H</userinput></para>
     <para>
@@ -771,7 +771,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_inversion">
-    <title>inversion &lt;term&gt;</title>
+    <title>inversion &term;</title>
     <titleabbrev>inversion</titleabbrev>
     <para><userinput>inversion t</userinput></para>
     <para>
@@ -806,7 +806,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_lapply">
-    <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
+    <title>lapply [depth=&nat;] &term; [to &lt;term list&gt;] [using &id;]</title>
     <titleabbrev>lapply</titleabbrev>
     <para><userinput>lapply ???</userinput></para>
     <para>
@@ -864,7 +864,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_letin">
-    <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
+    <title>letin &id; ≝ &term;</title>
     <titleabbrev>letin</titleabbrev>
     <para><userinput>letin x ≝ t</userinput></para>
     <para>
@@ -1004,7 +1004,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_replace">
-    <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
+    <title>replace &lt;pattern&gt; with &term;</title>
     <titleabbrev>change</titleabbrev>
     <para><userinput>change patt with t</userinput></para>
     <para>
@@ -1036,7 +1036,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_rewrite">
-    <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
+    <title>rewrite [&lt;|&gt;] &term; &lt;pattern&gt;</title>
     <titleabbrev>rewrite</titleabbrev>
     <para><userinput>rewrite dir p patt</userinput></para>
     <para>
@@ -1221,7 +1221,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_transitivity">
-    <title>transitivity &lt;term&gt;</title>
+    <title>transitivity &term;</title>
     <titleabbrev>transitivity</titleabbrev>
     <para><userinput>transitivity t</userinput></para>
     <para>
@@ -1250,7 +1250,7 @@ the current sequent to prove.</para>
     </para>
   </sect1>
   <sect1 id="tac_unfold">
-    <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
+    <title>unfold [&term;] &lt;pattern&gt;</title>
     <titleabbrev>unfold</titleabbrev>
     <para><userinput>unfold t patt</userinput></para>
     <para>
diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index e9402f237..93dd12bef 100644
--- a/matita/help/C/sec_terms.xml
+++ b/matita/help/C/sec_terms.xml
@@ -5,89 +5,199 @@
   <title>Terms, axioms, definitions, declarations and proofs</title>
 
   <sect1 id="terms">
-    <title>Terms</title>
-    <!--<informaltable>
-     <tr>
-      <td>&lt;term&gt;</td>
-      <td>::=</td>
-      <td>&lt;id&gt;</td>
-      <td>identifier</td>
-     </tr>
-     <tr><td/><td>|</td><td>&lt;term&gt; &lt;term&gt;</td>
-      <td>application</td></tr>
-    </informaltable>-->
-	<table>
-	  <tgroup>
-            <thead />
-	    <tbody>
-	      <row>
-		<entry>&lt;term&gt;</entry>
-		<entry>::=</entry>
-		<entry>&lt;id&gt;</entry>
-		<entry>identifier</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>&lt;term&gt; &lt;term&gt;</entry>
-		<entry>application</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>λ&lt;id&gt;[: &lt;term&gt;].&lt;term&gt;</entry>
-		<entry>λ-abstraction</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>Π&lt;id&gt;[: &lt;term&gt;].&lt;term&gt;</entry>
-		<entry>dependent product meant to define a datatype</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>∀&lt;id&gt;[: &lt;term&gt;].&lt;term&gt;</entry>
-		<entry>dependent product meant to define a proposition</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>&lt;term&gt; → &lt;term&gt;</entry>
-		<entry>non-dependent product (logical implication or function space)</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>let [&lt;id&gt;|(&lt;id&gt;: &lt;term&gt;)] ≝ &lt;term&gt; in &lt;term&gt;</entry>
-		<entry>local definition</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>let [co]rec &lt;id&gt; ≝ &lt;term&gt; in &lt;term&gt;</entry>
-		<entry>local definition</entry>
-	      </row>
-	      <row>
-		<entry/>
-		<entry>|</entry>
-		<entry>...</entry>
-		<entry>&TODO;</entry>
-	      </row>
-	    </tbody>
-	  </tgroup>
-	</table>
+  <title>Terms</title>
+  <table>
+    <tgroup>
+     <thead />
+    <tbody>
+     <row>
+      <entry id="id">&id;</entry>
+      <entry>::=</entry>
+      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+  <table>
+    <tgroup>
+     <thead />
+    <tbody>
+     <row>
+      <entry id="nat">&nat;</entry>
+      <entry>::=</entry>
+      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+  <table>
+    <tgroup>
+     <thead />
+    <tbody>
+     <row>
+      <entry id="uri">&uri;</entry>
+      <entry>::=</entry>
+      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+  <table>
+    <tgroup>
+     <thead />
+    <tbody>
+     <row>
+      <entry id="term">&term;</entry>
+      <entry>::=</entry>
+      <entry>&id;</entry>
+      <entry>identifier</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</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 predicatie sort of datatypes</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&term; &term;</entry>
+      <entry>application</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>
+     </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>
+     </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>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</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">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">match</emphasis> &term; 
+        [ <emphasis role="bold">in</emphasis> &term; ]
+        [ <emphasis role="bold">return</emphasis> &term; ]
+        <emphasis role="bold">with</emphasis>
+      </entry>
+      <entry>case analysis</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry/>
+      <entry>
+       <emphasis role="bold">[</emphasis> 
+       &term_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
+         [
+         <emphasis role="bold">|</emphasis>
+         &term_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>
+     </row>
+     <row>
+      <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;]…
+      </entry>
+      <entry/>
+     </row>
+     <row>
+      <entry/>
+      <entry/>
+      <entry>
+      <emphasis role="bold">in</emphasis> &term;
+      </entry>
+      <entry/>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+
+  <table>
+    <tgroup>
+     <thead />
+    <tbody>
+     <row>
+      <entry id="term_pattern">&term_pattern;</entry>
+      <entry>::=</entry>
+      <entry>&id;</entry>
+      <entry>0-ary constructor</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
+      <entry>n-ary constructor (binds the n arguments)</entry>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
   </sect1>
 
   <sect1 id="axiom">
-    <title>axiom &lt;id&gt;: &lt;term&gt;</title>
+    <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">
-    <title>definition &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
+    <title>definition &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>definition</titleabbrev>
     <para><userinput>definition f: T ≝ t</userinput></para>
     <para><command>f</command> is defined as <command>t</command>;
@@ -102,7 +212,7 @@
   </sect1>
 
   <sect1 id="inductive">
-    <title>[co]inductive &lt;id&gt; (of inductive types)</title>
+    <title>[co]inductive &id; (of inductive types)</title>
     <titleabbrev>(co)inductive types declaration</titleabbrev>
     <para> &TODO; </para>
   </sect1>
@@ -110,7 +220,7 @@
   <sect1 id="proofs">
    <title>Proofs</title>
    <sect2 id="theorem">
-    <title>theorem &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
+    <title>theorem &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>theorem</titleabbrev>
     <para><userinput>theorem f: P ≝ p</userinput></para>
     <para>Proves a new theorem <command>f</command> whose thesis is
@@ -127,7 +237,7 @@
     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
    </sect2>
    <sect2 id="variant">
-    <title>variant &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
+    <title>variant &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>variant</titleabbrev>
     <para><userinput>variant f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
@@ -135,19 +245,19 @@
      an alternative name or proof to a theorem.</para>
    </sect2>
    <sect2 id="lemma">
-    <title>lemma &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
+    <title>lemma &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>lemma</titleabbrev>
     <para><userinput>lemma f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
    </sect2>
    <sect2 id="fact">
-    <title>fact &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
+    <title>fact &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>fact</titleabbrev>
     <para><userinput>fact f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
    </sect2>
    <sect2 id="remark">
-    <title>remark &lt;id&gt;[: &lt;term&gt;] [≝ &lt;term&gt;]</title>
+    <title>remark &id;[: &term;] [≝ &term;]</title>
     <titleabbrev>remark</titleabbrev>
     <para><userinput>remark f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
-- 
2.39.2