X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=dbb6900d98f9d92d17184070315b0e7adf6d42f9;hb=68a413ec8a20ef0d73fcd5810be7db659abe6f92;hp=9a968e5c970baccfceeb48f07ee7f85c1498926f;hpb=68aad189a157255485177a8a632d44ac3ad73a09;p=helm.git
diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index 9a968e5c9..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;
@@ -601,18 +636,18 @@
&pattern;
::=
- {
+ in
[&id;[: &path;]]â¦
- [⢠&path;]]}
+ [⢠&path;]];
simple pattern
|
- {match &path;
+ in match &path;
[in
[&id;[: &path;]]â¦
- [⢠&path;]]}
+ [⢠&path;]];
full pattern
@@ -620,7 +655,7 @@