Manual(s) fixed and committed to avoid rebuilding them in dune

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

diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index 9a968e5c970baccfceeb48f07ee7f85c1498926f..67603c55d53cac6c206e61d1a9fa80da749223f8 100644 (file)
--- a/matita/matita/help/C/sec_terms.xml
+++ b/matita/matita/help/C/sec_terms.xml
@@ -453,6 +453,41 @@
      <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="discriminator">
+    <title><emphasis role="bold">discriminator</emphasis> &id;</title>
+    <titleabbrev>discriminator</titleabbrev>
+    <para><userinput>discriminator i</userinput></para>
+    <para>Defines a new discrimination (injectivity+conflict) principle à la 
+     McBride for the inductive type <command>i</command>.</para> 
+    <para>The principle will use John 
+     Major's equality if such equality is defined, otherwise it will use 
+     Leibniz equality; in the former case, it will be called 
+     <command>i_jmdiscr</command>, in the latter, <command>i_discr</command>. 
+     The command will fail if neither equality is available.</para>   
+    <para>Discrimination principles are used by the destruct tactic and are 
+     usually automatically generated by Matita during the definition of the 
+     corresponding inductive type. This command is thus especially useful 
+     when the correct equality was not loaded at the time of that 
+     definition.</para>
+  </sect2>
+  <sect2 id="inverter">
+    <title><emphasis role="bold">inverter</emphasis> &id; <emphasis role="bold">for</emphasis> &id; (&path;) [&term;]</title>
+    <titleabbrev>inverter</titleabbrev>
+    <para><userinput>inverter n for i (path) : s</userinput></para>
+    <para>Defines a new induction/inversion principle for the inductive type
+     <command>i</command>, called <command>n</command>.</para>
+    <para><command>(path)</command> must be in the form <command>(# # # ... #)</command>, 
+     where each <command>#</command> can be either <command>?</command> or 
+     <command>%</command>, and the number of symbols is equal to the number of 
+     right parameters (indices) of <command>i</command>. Parentheses are 
+     mandatory. If the j-th symbol is 
+     <command>%</command>, Matita will generate a principle providing 
+     equations for reasoning on the j-th index of <command>i</command>. If the
+     symbol is a <command>?</command>, no corresponding equation will be 
+     provided.</para>
+    <para><command>s</command>, which must be a sort, is the target sort of the
+     induction/inversion principle and defaults to <command>Prop</command>.</para>
+  </sect2>
   <sect2 id="letrec">
     <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
     <titleabbrev>&TODO;</titleabbrev>
@@ -601,18 +636,18 @@
        <row>
        <entry id="grammar.pattern">&pattern;</entry>
        <entry>::=</entry>
-        <entry><emphasis role="bold">{</emphasis>
+        <entry><emphasis role="bold">in</emphasis>
           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
-          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
         <entry>simple pattern</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">{match</emphasis> &path;
+        <entry><emphasis role="bold">in</emphasis> <emphasis role="bold">match</emphasis> &path;
           [<emphasis role="bold">in</emphasis>
           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
-          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
         <entry>full pattern</entry>
        </row>
       </tbody>
@@ -620,7 +655,7 @@
     </table>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>path</title>
-      <tgroup cols="4">
+      <tgroup cols="3">
       <tbody>
        <row>
        <entry id="grammar.path">&path;</entry>
@@ -814,7 +849,6 @@
     </table>
     </sect2>
 
-    <!--
     <sect2 id="justification">
     <title>justification</title>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
@@ -837,7 +871,6 @@
      </tgroup>
     </table>
     </sect2>
-    -->
   </sect1>
 
 </chapter>