X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=05385f666b3a41ad4267a1977c0e8c8dac9aa4d5;hb=a1a8ac61970fce48a3e0c8fa673a70a03e026c50;hp=f5ac2b3ec1d7667d508fe2b7c71f07eb29f9f011;hpb=be292a08ee0c8792b21105952626da05d5f645b9;p=helm.git

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index f5ac2b3ec..05385f666 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -198,7 +198,7 @@
 	<entry id="grammar.rec_def">&rec_def;</entry>
 	<entry>::=</entry>
 	<entry>
-	  &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
+	  &id; [&id;|<emphasis role="bold">_</emphasis>|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
 	</entry>
 	<entry />
       </row>
@@ -285,7 +285,7 @@
       <entry/>
       <entry>|</entry>
         <entry><emphasis role="bold">match</emphasis> &term; 
-        [ <emphasis role="bold">in</emphasis> &term; ]
+        [ <emphasis role="bold">in</emphasis> &id; ]
         [ <emphasis role="bold">return</emphasis> &term; ]
         <emphasis role="bold">with</emphasis>
       </entry>
@@ -387,6 +387,12 @@
       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
       <entry>n-ary constructor (binds the n arguments)</entry>
      </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&id; &id; [&id;]…</entry>
+      <entry>n-ary constructor (binds the n arguments)</entry>
+     </row>
     </tbody>
    </tgroup>
   </table>
@@ -417,6 +423,11 @@
      <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>
   </sect2>
+  <sect2 id="letrec">
+    <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
+    <titleabbrev>&TODO;</titleabbrev>
+    <para>&TODO;</para>
+  </sect2>
   <sect2 id="inductive">
     <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;]…]…