X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2;hb=871ed1c297e8c929a8c4460162e8521c9656bbc0;hp=e9c1c054cc0201704491cbc5bc09cc56dc309842;hpb=53d918bdbe4135cee1764f27f5c5c8a585bf3481;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index e9c1c054c..fbf8dd4ef 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -5,62 +5,67 @@ Syntax To describe syntax in this manual we use the following conventions: - Non terminal symbols are emphasized and have a link to their definition. E.g.: &term; - Terminal symbols are in bold. E.g.: theorem - Optional sequences of elements are put in square brackets. - E.g.: [in &term;] - Alternatives are put in square brakets and they are separated - by vertical bars. E.g.: [<|>] - Repetition of sequences of elements are given by putting the + Non terminal symbols are emphasized and have a link to their + definition. E.g.: &term; + Terminal symbols are in bold. E.g.: + theorem + Optional sequences of elements are put in square brackets. + E.g.: [in &term;] + Alternatives are put in square brakets and they are + separated by vertical bars. E.g.: [<|>] + Repetition of sequences of elements are given by putting the first sequence in square brackets, that are followed by three dots. - E.g.: [and &term;]… + E.g.: [and &term;]… Terms & co. Lexical conventions - - - - - - &id; - ::= - 〈〈&TODO;〉〉 - - - -
- - - - - - &nat; - ::= - 〈〈&TODO;〉〉 - - - -
- - - - - - &uri; - ::= - 〈〈&TODO;〉〉 - - - -
+ + + id + + + + &id; + ::= + 〈〈&TODO;〉〉 + + + +
+ + nat + + + + &nat; + ::= + 〈〈&TODO;〉〉 + + + +
+ + uri + + + + &uri; + ::= + 〈〈&TODO;〉〉 + + + +
+ Terms - + +
+ Terms - &term; @@ -144,9 +149,9 @@
- +
+ Simple terms - &sterm; @@ -241,9 +246,9 @@
- +
+ Arguments - &args; @@ -277,9 +282,9 @@
- +
+ Miscellaneous arguments - &args2; @@ -297,9 +302,9 @@
- +
+ Pattern matching - &match_pattern; @@ -316,6 +321,7 @@
+ @@ -343,9 +349,30 @@ Notice that the command is equivalent to theorem f: T ≝ t. - [co]inductive &id; (of inductive types) + [<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;]…]… + (co)inductive types declaration - &TODO; + inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm' + Declares a family of two mutually inductive types + i and i' whose types are + S and S', which must be convertible + to sorts. + The constructors ki of type Ti + and ki' of type Ti' are also + simultaneously declared. The declared types i and + i' may occur in the types of the constructors, but + only in strongly positive positions according to the rules of the + calculus. + The whole family is parameterized over the arguments x,y,z. + If the keyword coinductive is used, the declared + types are considered mutually coinductive. + Elimination principles for the record are automatically generated + by Matita, if allowed by the typing rules of the calculus according to + the sort S. If generated, + they are named i_ind, i_rec and + i_rect according to the sort of their induction + predicate. <emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;]…<emphasis role="bold">}</emphasis> @@ -360,8 +387,8 @@ Elimination principles for the record are automatically generated by Matita, if allowed by the typing rules of the calculus according to the sort S. If generated, - they are named id_ind, id_rec and - id_rect according to the sort of their induction + they are named i_ind, i_rec and + i_rect according to the sort of their induction predicate. For each field fi a record projection fi is also automatically generated if projection