X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=dbf1718f8f3a4f0013dcfccf29fc94faa7eef706;hb=f63e9358746f82de0dd07d60bdf82fdc0fae2101;hp=d521ac87060a6a2e0a462fd8ae079e2235184696;hpb=48aa99d1d9659e55d68ab3ef50b10bc6165eee03;p=helm.git
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index d521ac870..dbf1718f8 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -26,6 +26,18 @@
Terms & co.
Lexical conventions
+
+ qstring
+
+
+
+ &qstring;
+ ::=
+ "â©â©any sequence of characters excluded "âªâª"
+
+
+
+
id
@@ -186,7 +198,7 @@
&rec_def;
::=
- &id; [&id;|(&id;[,&term;]⦠:&term;)]â¦
+ &id; [&id;|_|(&id;[,&id;]⦠:&term;)]â¦
@@ -194,7 +206,7 @@
- [on &nat;]
+ [on &id;]
[: &term;]
â &term;]
@@ -273,7 +285,7 @@
|
match &term;
- [ in &term; ]
+ [ in &id; ]
[ return &term; ]
with
@@ -375,6 +387,18 @@
(&id; &id; [&id;]â¦)
n-ary constructor (binds the n arguments)
+
+
+ |
+ &id; &id; [&id;]â¦
+ n-ary constructor (binds the n arguments)
+
+
+
+ |
+ _
+ any remaining constructor (ignoring its arguments)
+
@@ -405,6 +429,11 @@
f must be defined by means of tactics.
Notice that the command is equivalent to theorem f: T â t.
+
+ <emphasis role="bold">letrec</emphasis> &TODO;
+ &TODO;
+ &TODO;
+
[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]⦠<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">â</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]â¦
[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">â</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]â¦]â¦
@@ -545,7 +574,7 @@
<row>
<entry/>
<entry>|</entry>
- <entry><emphasis role="bold">in match</emphasis> &term;
+ <entry><emphasis role="bold">in match</emphasis> &path;
[<emphasis role="bold">in</emphasis>
[&id;[<emphasis role="bold">:</emphasis> &path;]]â¦
[<emphasis role="bold">â¢</emphasis> &path;]]</entry>
@@ -561,7 +590,7 @@
<row>
<entry id="grammar.path">&path;</entry>
<entry>::=</entry>
- <entry><emphasis>â©â©any &sterm; whithout occurrences of <emphasis role="bold">Set</emphasis>, <emphasis role="bold">Prop</emphasis>, <emphasis role="bold">CProp</emphasis>, <emphasis role="bold">Type</emphasis>, &id;, &uri; and user provided notation; however, <emphasis role="bold">%</emphasis> is now an additional production for &sterm;âªâª</emphasis></entry>
+ <entry><emphasis>â©â©any &sterm; without occurrences of <emphasis role="bold">Set</emphasis>, <emphasis role="bold">Prop</emphasis>, <emphasis role="bold">CProp</emphasis>, <emphasis role="bold">Type</emphasis>, &id;, &uri; and user provided notation; however, <emphasis role="bold">%</emphasis> is now an additional production for &sterm;âªâª</emphasis></entry>
</row>
</tbody>
</tgroup>
@@ -574,6 +603,26 @@
that can be represented by <emphasis role="bold">?</emphasis>.
</para></listitem>
</orderedlist>
+ <para>Warning: the format for a path for a <emphasis role="bold">match</emphasis> ⦠<emphasis role="bold">with</emphasis>
+ expression is restricted to: <emphasis role="bold">match</emphasis> &path;
+ <emphasis role="bold">with</emphasis>
+ <emphasis role="bold">[</emphasis>
+ <emphasis role="bold">_</emphasis>
+ <emphasis role="bold">â</emphasis>
+ &path;
+ <emphasis role="bold">|</emphasis> â¦
+ <emphasis role="bold">|</emphasis>
+ <emphasis role="bold">_</emphasis>
+ <emphasis role="bold">â</emphasis>
+ &path;
+ <emphasis role="bold">]</emphasis>
+ Its semantics is the following: the n-th
+ "<emphasis role="bold">_</emphasis>
+ <emphasis role="bold">â</emphasis>
+ &path;" branch is matched against the n-th constructor of the
+ inductive data type. The head λ-abstractions of &path; are matched
+ against the corresponding constructor arguments.
+ </para>
<para>For instance, the path
<userinput>â_,_:?.(? ? % ?)â(? ? ? %)</userinput>
locates at once the subterms
@@ -643,11 +692,6 @@
<row>
<entry id="grammar.reduction-kind">&reduction-kind;</entry>
<entry>::=</entry>
- <entry><emphasis role="bold">demodulate</emphasis></entry>
- </row>
- <row>
- <entry/>
- <entry>|</entry>
<entry><emphasis role="bold">normalize</emphasis></entry>
<entry>Computes the βδιζ-normal form</entry>
</row>
@@ -680,6 +724,95 @@
</tgroup>
</table>
</sect2>
+
+ <sect2 id="auto-params">
+ <title>auto-params
+
+ auto-params
+
+
+
+ &autoparams;
+ ::=
+ [&simpleautoparam;]â¦
+ [by
+ &term; [,&term;]â¦]
+
+
+
+
+
+
+ simple-auto-param
+
+
+
+ &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)
+
+
+
+ |
+ type
+ Try to close also goals of sort Type, otherwise only goals
+ living in sort Prop are attacked.
+
+
+
+
+ |
+ paramodulation
+ Try to close the goal performing unit-equality paramodulation
+
+
+
+
+ |
+ timeout=&nat;
+ Timeout in seconds
+
+
+
+
+
+
+
+
+ justification
+
+ justification
+
+
+
+ &justification;
+ ::=
+ using &term;
+ Proof term manually provided
+
+
+
+ |
+ &autoparams;
+ Call automation
+
+
+
+
+