From: Claudio Sacerdoti Coen Date: Fri, 20 Jun 2008 12:02:13 +0000 (+0000) Subject: Further documentation for notation. X-Git-Tag: make_still_working~5007 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5591e27a010ba6eb06cbd61b5b22358f2d572871;p=helm.git Further documentation for notation. --- diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index 21dd9bc7b..1e45ce844 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -60,8 +60,11 @@ csymbol"> usage"> notation_lhs"> + layout"> + literal"> notation_rhs"> associativity"> + symbol"> ]> diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 082a5bb75..287267bd6 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -109,7 +109,19 @@ - + + + symbol + + + + &symbol; + ::= + 〈〈None of the above〉〉 + + + +
Terms diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml index 46bf146c9..734e95692 100644 --- a/helm/software/matita/help/C/sec_usernotation.xml +++ b/helm/software/matita/help/C/sec_usernotation.xml @@ -118,12 +118,187 @@ ¬ation_lhs; ::= - &TODO; - &TODO; + &layout; [&layout;]… - + + + + layout + + + + &layout; + ::= + &layout; \sub &layout; + Subscript + + + + | + &layout; \sup &layout; + Superscript + + + + | + &layout; \below &layout; + + + + + | + &layout; \above &layout; + + + + + | + &layout; \over &layout; + + + + + | + &layout; \atop &layout; + + + + + | + \frac &layout; &layout; + Fraction + + + + | + \sqrt &layout; + Square root + + + + | + \root &layout; \of &layout; + Generalized root + + + + | + hbox ( &layout; [&layout;]… ) + Horizontal box + + + + | + vbox ( &layout; [&layout;]… ) + Vertical box + + + + | + hvbox ( &layout; [&layout;]… ) + Horizontal and vertical box + + + + | + hovbox ( &layout; [&layout;]… ) + Horizontal or vertical box + + + + | + break + Breakable space + + + + | + ( &layout; [&layout;]… ) + Group + + + + | + &id; + Placeholder for a term with no explicit precedence + + + + | + term &nat; &id; + Placeholder for a term with explicit expected precedence + + + + | + number &id; + Placeholder for a natural number + + + + | + ident &id; + Placeholder for an identifier + + + + | + &literal; + Literal + + + + | + opt &layout; + Optional layout (it can be omitted for parsing) + + + + | + list0 &layout; + [sep &literal;] + List of layouts separated by sep (default: + any blank) + + + + | + list1 &layout; + [sep &literal;] + Non empty list of layouts separated by sep + (default: any blank) + + + +
+ + + literal + + + + &literal; + ::= + &symbol; + Unicode symbol + + + + | + &nat; + Natural number (a constant) + + + + | + '&id;' + New keyword for the lexer + + + +