X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=dbb6900d98f9d92d17184070315b0e7adf6d42f9;hb=2dc6df301ca3ebf444ec7f767921ee0e57ccd592;hp=a1353b2f021aac59be2fe0896c2fbd827ab2795d;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git
diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index a1353b2f0..dbb6900d9 100644
--- a/matita/matita/help/C/sec_terms.xml
+++ b/matita/matita/help/C/sec_terms.xml
@@ -453,6 +453,41 @@
f must be defined by means of tactics.
Notice that the command is equivalent to theorem f: T â t.
+
+ discriminator &id;
+ discriminator
+ discriminator i
+ Defines a new discrimination (injectivity+conflict) principle à la
+ McBride for the inductive type i.
+ 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
+ i_jmdiscr, in the latter, i_discr.
+ The command will fail if neither equality is available.
+ 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.
+
+
+ inverter &id; for &id; (&path;) [&term;]
+ inverter
+ inverter n for i (path) : s
+ Defines a new induction/inversion principle for the inductive type
+ i, called n.
+ (path) must be in the form (# # # ... #),
+ where each # can be either ? or
+ %, and the number of symbols is equal to the number of
+ right parameters (indices) of i. Parentheses are
+ mandatory. If the j-th symbol is
+ %, Matita will generate a principle providing
+ equations for reasoning on the j-th index of i. If the
+ symbol is a ?, no corresponding equation will be
+ provided.
+ s, which must be a sort, is the target sort of the
+ induction/inversion principle and defaults to Prop.
+
letrec &TODO;
&TODO;
@@ -524,13 +559,15 @@
P. Otherwise an interactive proof is started.
P can be omitted only if the proof is not
interactive.
+
A warning is raised if the name of the theorem cannot be obtained
by mangling the name of the constants in its thesis.
Notice that the command is equivalent to definition f: T â t.
+
+
+ corollary &id;[: &term;] [â &term;]
+ corollary
+ corollary f: T â t
+ Same as theorem f: T â t
lemma &id;[: &term;] [â &term;]
@@ -551,11 +594,12 @@
fact f: T â t
Same as theorem f: T â t
-