X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=11b06b21cab7269c8bd3bd2867ed8bc48b31f1c5;hb=21f2ca1e83578359d9ab6926d466a4645049ee76;hp=fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2;hpb=871ed1c297e8c929a8c4460162e8521c9656bbc0;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index fbf8dd4ef..11b06b21c 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -13,62 +13,103 @@ 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. + Repetitions of a sequence of elements are given by putting the + sequence in square brackets, that are followed by three dots. The empty + sequence is a valid repetition. E.g.: [and &term;]… + Characters belonging to a set of characters are given + by listing the set elements in square brackets. Hyphens are used to + specify ranges of characters in the set. + E.g.: [a-zA-Z0-9_-] Terms & co. Lexical conventions - - +
id - &id; + &id; ::= - 〈〈&TODO;〉〉 + 〈〈any sequence of letters, underscores or valid XML digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉
- +
nat - &nat; + &nat; + ::= + 〈〈any sequence of valid XML digits〉〉 + + + +
+ + char + + + + &char; ::= - 〈〈&TODO;〉〉 + [a-zA-Z0-9_-]
- +
+ uri-step + + + + &uri-step; + ::= + &char;[&char;]… + + + +
+ uri - &uri; + &uri; ::= - 〈〈&TODO;〉〉 + [cic:/|theory:/]&uri-step;[/&uri-step;]….&id;[.&id;]…[#xpointer(&nat;/&nat;[/&nat;]…)]
- Terms + + + + - +
Terms - &term; + &term; ::= &sterm; simple or delimited term @@ -112,11 +153,10 @@ | - let - [co]rec - &id; [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term; + + let + [co]rec + &rec_def; (co)recursive definitions @@ -124,10 +164,7 @@ - [and - [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term;]… + [and &rec_def;]… @@ -145,16 +182,34 @@ …user provided notation + + &rec_def; + ::= + + &id; [&id;|(&id;[,&term;]… :&term;)]… + + + + + + + + [on &nat;] + [: &term;] + ≝ &term;] + + +
- +
Simple terms - &sterm; + &sterm; ::= (&term;) @@ -223,11 +278,9 @@ [ - &match_pattern; ⇒ &term; - [ - | - &match_pattern; ⇒ &term; - ]…] + &match_branch;[|&match_branch;]… + ] + @@ -246,12 +299,12 @@
- +
Arguments - &args; + &args; ::= _[: &term;] @@ -278,16 +331,8 @@ (&id;[,&id;]…[: &term;]) - - -
- - - Miscellaneous arguments - - - &args2; + &args2; ::= &id; @@ -302,12 +347,18 @@
- +
Pattern matching + + &match_branch; + ::= + &match_pattern; ⇒ &term; + + - &match_pattern; + &match_pattern; ::= &id; 0-ary constructor @@ -449,5 +500,95 @@ + + Tactic arguments + This section documents the syntax of some recurring arguments for + tactics. + + + intros-spec +
+ intros-spec + + + + &intros-spec; + ::= + [&nat;] [([&id;]…)] + + + +
+ The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses. + + + + pattern + + pattern + + + + &pattern; + ::= + &TODO; + + + +
+ &TODO; + + + + reduction-kind + Reduction kinds are normalization functions that transform a term + to a convertible but simpler one. Each reduction kind can be used both + as a tactic argument and as a stand-alone tactic. + + reduction-kind + + + + &reduction-kind; + ::= + demodulate + + + + | + normalize + Computes the βδιζ-normal form + + + + | + reduce + Computes the βδιζ-normal form + + + + | + simplify + Computes a form supposed to be simpler + + + + | + unfold [&sterm;] + δ-reduces the constant or variable if specified, or that + in head position + + + + | + whd + Computes the βδιζ-weak-head normal form + + + +
+ + +