From b4fb4fa6c17945b70d821e2b31e6aca727bcf9d5 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 May 2006 13:41:55 +0000
Subject: [PATCH] More documentation.

---
 helm/software/matita/help/C/matita.xml      |   4 +-
 helm/software/matita/help/C/sec_tactics.xml |  34 ++--
 helm/software/matita/help/C/sec_terms.xml   | 166 +++++++++++++++-----
 3 files changed, 143 insertions(+), 61 deletions(-)

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 14411ad71..1120cb4ec 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -24,7 +24,9 @@
   <!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>">
+  <!ENTITY match_pattern "<emphasis><link linkend='match_pattern'>match_pattern</link></emphasis>">
+  <!ENTITY args "<emphasis><link linkend='args'>args</link></emphasis>">
+  <!ENTITY sterm "<emphasis><link linkend='sterm'>sterm</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index fb695879f..96e56494c 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -4,7 +4,7 @@
  <title>Tactics</title>
 
   <sect1 id="tac_absurd">
-    <title>absurd &term;</title>
+    <title>absurd &sterm;</title>
     <titleabbrev>absurd</titleabbrev>
     <para><userinput>absurd P</userinput></para>
      <para>
@@ -33,7 +33,7 @@
      </para>
   </sect1>
   <sect1 id="tac_apply">
-    <title>apply &term;</title>
+    <title>apply &sterm;</title>
     <titleabbrev>apply</titleabbrev>
     <para><userinput>apply t</userinput></para>
     <para>
@@ -188,7 +188,7 @@
     </para>
   </sect1>
   <sect1 id="tac_change">
-    <title>change &lt;pattern&gt; with &term;</title>
+    <title>change &lt;pattern&gt; with &sterm;</title>
     <titleabbrev>change</titleabbrev>
     <para><userinput>change patt with t</userinput></para>
     <para>
@@ -281,7 +281,7 @@
     </para>
   </sect1>
   <sect1 id="tac_cut">
-    <title>cut &term; [as &id;]</title>
+    <title>cut &sterm; [as &id;]</title>
     <titleabbrev>cut</titleabbrev>
     <para><userinput>cut P as H</userinput></para>
     <para>
@@ -339,7 +339,7 @@
     </para>
   </sect1>
   <sect1 id="tac_discriminate">
-    <title>discriminate &term;</title>
+    <title>discriminate &sterm;</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 &term; [using &term;] [&lt;intros_spec&gt;]</title>
+    <title>elim &sterm; [using &sterm;] [&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 &term; [using &term;] [&lt;intros_spec&gt;]</title>
+    <title>elimType &sterm; [using &sterm;] [&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 &term;</title>
+    <title>exact &sterm;</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; &term; &lt;pattern&gt;</title>
+    <title>fold &lt;reduction_kind&gt; &sterm; &lt;pattern&gt;</title>
     <titleabbrev>fold</titleabbrev>
     <para><userinput>fold red t patt</userinput></para>
     <para>
@@ -670,7 +670,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_injection">
-    <title>injection &term;</title>
+    <title>injection &sterm;</title>
     <titleabbrev>injection</titleabbrev>
     <para><userinput>injection p</userinput></para>
     <para>
@@ -771,7 +771,7 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_inversion">
-    <title>inversion &term;</title>
+    <title>inversion &sterm;</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=&nat;] &term; [to &lt;term list&gt;] [using &id;]</title>
+    <title>lapply [depth=&nat;] &sterm; [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 &id; ≝ &term;</title>
+    <title>letin &id; ≝ &sterm;</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 &term;</title>
+    <title>replace &lt;pattern&gt; with &sterm;</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;] &term; &lt;pattern&gt;</title>
+    <title>rewrite [&lt;|&gt;] &sterm; &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 &term;</title>
+    <title>transitivity &sterm;</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 [&term;] &lt;pattern&gt;</title>
+    <title>unfold [&sterm;] &lt;pattern&gt;</title>
     <titleabbrev>unfold</titleabbrev>
     <para><userinput>unfold t patt</userinput></para>
     <para>
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 3171544a2..45459572b 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -65,68 +65,143 @@
      <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 predicative 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>
+     <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/>
@@ -143,42 +218,46 @@
       <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>
-      [<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/>
+      <entry>|</entry>
+      <entry>…</entry>
+      <entry>user provided notation at precedence 90</entry>
      </row>
+    </tbody>
+   </tgroup>
+  </table>
+
+  <table>
+    <tgroup>
+     <thead />
+    <tbody>
      <row>
-      <entry/>
-      <entry/>
+      <entry id="args">&args;</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>[<emphasis role="bold">(</emphasis>]&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]</entry>
+      <entry></entry>
      </row>
     </tbody>
    </tgroup>
@@ -189,7 +268,7 @@
      <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>
@@ -203,6 +282,7 @@
     </tbody>
    </tgroup>
   </table>
+
   </sect2>
   </sect1>
 
-- 
2.39.2