X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=67603c55d53cac6c206e61d1a9fa80da749223f8;hb=c2ae3d595414cd5e7f841330cbba57b56af925c5;hp=8e680bb7cb7e83d9133383cd6eb6b3590d1c0e4c;hpb=8f699ab265e380a2d1ab7dba0ee5e8ba5556a84a;p=helm.git
diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index 8e680bb7c..67603c55d 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.
+
+ <emphasis role="bold">discriminator</emphasis> &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.
+
+
+ <emphasis role="bold">inverter</emphasis> &id; <emphasis role="bold">for</emphasis> &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.
+
<emphasis role="bold">letrec</emphasis> &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 @@
path
-
+
&path;
@@ -752,9 +787,20 @@
&autoparams;
::=
- [&simpleautoparam;]â¦
+ [&nat;] [&simpleautoparam;]â¦
[by
- &term; [,&term;]â¦]
+ [&sterm;⦠| _]]
+
+ The natural number, which defaults to 1, gives a bound to
+ the depth of the search tree. The terms listed is the only
+ knowledge base used by automation together with all indexed factual
+ and equational theorems in the included library. If the list of terms
+ is empty, only equational theorems and facts in the library are
+ used. If the list is omitted, it defaults to all indexed theorems
+ in the library. Finally, if the list is _,
+ the automation command becomes a macro that is expanded in a new
+ automation command where _ is replaced with the
+ list of theorems required to prove the sequent.
@@ -767,47 +813,35 @@
&simpleautoparam;
::=
- depth=&nat;
- Give a bound to the depth of the search tree
-
-
-
- |
width=&nat;
The maximal width of the search tree
|
- library
- Search everywhere (not only in included files)
+ size=&nat;
+ The maximal number of nodes in the proof
|
- type
- Try to close also goals of sort Type, otherwise only goals
- living in sort Prop are attacked.
+ demod
+ Simplifies the current sequent using the current set of
+ equations known to automation
|
- paramodulation
+ paramod
Try to close the goal performing unit-equality paramodulation
|
- size=&nat;
- The maximal number of nodes in the proof
-
-
-
- |
- timeout=&nat;
- Timeout in seconds
+ fast_paramod
+ A bounded version of paramod that is granted to terminate quickly
@@ -815,7 +849,6 @@
-