just a Pcre expression fixed, nothing real

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

diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index f5ac2b3ec1d7667d508fe2b7c71f07eb29f9f011..05385f666b3a41ad4267a1977c0e8c8dac9aa4d5 100644 (file)
--- a/matita/help/C/sec_terms.xml
+++ b/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;]…]…