From fef56ebd0e6b5edd2fe8b3393288c8811a7afc43 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 18 Nov 2011 16:02:48 +0000
Subject: [PATCH] Added help for discriminator and inverter.

---
 matita/matita/help/C/sec_terms.xml | 35 ++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index 9a968e5c9..8cd75e228 100644
--- 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>
-- 
2.39.2