From: Claudio Sacerdoti Coen Date: Fri, 9 Jun 2006 14:33:16 +0000 (+0000) Subject: Lexical conventions documented. X-Git-Tag: 0.4.95@7852~1354 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fbdf01e49ca301b3dbf1ddb3c4e358d8189e45c;p=helm.git Lexical conventions documented. --- diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml index 8934ffffd..7b3b3d30c 100644 --- a/matita/help/C/matita.xml +++ b/matita/help/C/matita.xml @@ -25,6 +25,8 @@ id"> uri"> + char"> + uri-step"> nat"> term"> match_pattern"> diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index fbf8dd4ef..f7991374c 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -13,8 +13,9 @@ 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;]… @@ -29,7 +30,7 @@ &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 ([?'`])〉〉 @@ -41,7 +42,31 @@ &nat; ::= - 〈〈&TODO;〉〉 + 〈〈any sequence of valid XML digits + + + + + + char + + + + &char; + ::= + [a-zA-Z0-9_-] + + + +
+ + uri-step + + + + &uri-step; + ::= + &char;[&char;]… @@ -53,7 +78,7 @@ &uri; ::= - 〈〈&TODO;〉〉 + [cic:/|theory:/]&uri-step;[/&uri-step;]….&id;[.&id;]…[#xpointer(&nat;/&nat;[/&nat;]…)]