Added new ternary layout \infrule premises conclusion name.

[helm.git] / helm / software / matita / help / C / sec_usernotation.xml

diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index 46bf146c97d684bafb5c180a9fd648917484ac02..1076338e6e06050d6702f29f3acb360e6c9873f8 100644 (file)
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -84,7 +84,7 @@
        <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
+        <entry><emphasis role="bold">right</emphasis> <emphasis role="bold">associative</emphasis></entry>
         <entry>Right associative</entry>
        </row>
        <row>
@@ -104,7 +104,13 @@
        <row>
         <entry id="grammar.notation_rhs">&notation_rhs;</entry>
         <entry>::=</entry>
+        <entry>&unparsed_ast;</entry>
         <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&unparsed_meta;</entry>
         <entry>&TODO;</entry>
        </row>
       </tbody>
@@ -112,19 +118,340 @@
      </table>
 
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
-      <title>notation_lhs</title>
+      <title>unparsed_ast</title>
       <tgroup cols="4">
       <tbody>
        <row>
-        <entry id="grammar.notation_lhs">&notation_lhs;</entry>
+        <entry id="grammar.unparsed_ast">&unparsed_ast;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">@{</emphasis>&enriched_term;<emphasis role="bold">}</emphasis></entry>
+        <entry>A content level AST (a term which is parsed, but not disambiguated).</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">@</emphasis>&id;</entry>
+        <entry><command>@id</command> is just an abbreviation for <command>@{id}</command></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">@</emphasis>&csymbol;</entry>
+        <entry><command>@'symbol</command> is just an abbreviation for <command>@{'symbol}</command></entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>enriched_term</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.enriched_term">&enriched_term;</entry>
+        <entry>::=</entry>
+        <entry>〈〈A term that may contain occurrences of &unparsed_meta;, even as variable names in binders, and occurrences of &csymbol;〉〉</entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>unparsed_meta</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.unparsed_meta">&unparsed_meta;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">${</emphasis>&level2_meta;<emphasis role="bold">}</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">$</emphasis>&id;</entry>
+        <entry><command>$id</command> is just an abbreviation for <command>${id}</command></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">$</emphasis><emphasis role="bold">_</emphasis></entry>
+        <entry><command>$_</command> is just an abbreviation for <command>${_}</command></entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>level2_meta</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.level2_meta">&level2_meta;</entry>
         <entry>::=</entry>
+        <entry>&unparsed_ast;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">term</emphasis> &nat; &id;</entry>
         <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">number</emphasis> &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">ident</emphasis> &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">fresh</emphasis> &id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">anonymous</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&id;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">fold</emphasis> [<emphasis role="bold">left</emphasis>|<emphasis role="bold">right</emphasis>] &level2_meta; <emphasis role="bold">rec</emphasis> &id; &level2_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">default</emphasis> &level2_meta; &level2_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">if</emphasis> &level2_meta; <emphasis role="bold">then</emphasis> &level2_meta; <emphasis role="bold">else</emphasis> &level2_meta;</entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">fail</emphasis></entry>
         <entry>&TODO;</entry>
        </row>
       </tbody>
       </tgroup>
      </table>
 
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>notation_lhs</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.notation_lhs">&notation_lhs;</entry>
+        <entry>::=</entry>
+        <entry>&layout; [&layout;]…</entry>
+       </row>
+      </tbody>
+      </tgroup>
+    </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>layout</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.layout">&layout;</entry>
+        <entry>::=</entry>
+        <entry>&layout; <emphasis role="bold">\sub</emphasis> &layout;</entry>
+        <entry>Subscript</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\sup</emphasis> &layout;</entry>
+        <entry>Superscript</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\below</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\above</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\over</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&layout; <emphasis role="bold">\atop</emphasis> &layout;</entry>
+        <entry></entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\frac</emphasis> &layout; &layout;</entry>
+        <entry>Fraction</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\infrule</emphasis> &layout; &layout; &layout;</entry>
+        <entry>Inference rule (premises, conclusion, rule name)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\sqrt</emphasis> &layout;</entry>
+        <entry>Square root</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">\root</emphasis> &layout; <emphasis role="bold">\of</emphasis> &layout;</entry>
+        <entry>Generalized root</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">hbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Horizontal box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">vbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Vertical box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">hvbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Horizontal and vertical box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">hovbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Horizontal or vertical box</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">break</emphasis></entry>
+        <entry>Breakable space</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
+        <entry>Group</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&id;</entry>
+        <entry>Placeholder for a term with no explicit precedence</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">term</emphasis> &nat; &id;</entry>
+        <entry>Placeholder for a term with explicit expected precedence</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">number</emphasis> &id;</entry>
+        <entry>Placeholder for a natural number</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">ident</emphasis> &id;</entry>
+        <entry>Placeholder for an identifier</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&literal;</entry>
+        <entry>Literal</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">opt</emphasis> &layout;</entry>
+        <entry>Optional layout (it can be omitted for parsing)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">list0</emphasis> &layout;
+               [<emphasis role="bold">sep</emphasis> &literal;]</entry>
+        <entry>List of layouts separated by <command>sep</command> (default:
+               any blank)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">list1</emphasis> &layout;
+               [<emphasis role="bold">sep</emphasis> &literal;]</entry>
+        <entry>Non empty list of layouts separated by <command>sep</command>
+               (default: any blank)</entry>
+       </row>
+      </tbody>
+      </tgroup>
+    </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>literal</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.literal">&literal;</entry>
+        <entry>::=</entry>
+        <entry>&symbol;</entry>
+        <entry>Unicode symbol</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry>&nat;</entry>
+        <entry>Natural number (a constant)</entry>
+       </row>
+       <row>
+        <entry></entry>
+        <entry>|</entry>
+        <entry><emphasis role="bold">&apos;</emphasis>&id;<emphasis role="bold">&apos;</emphasis></entry>
+        <entry>New keyword for the lexer</entry>
+       </row>
+      </tbody>
+      </tgroup>
+    </table>
+
         </listitem>
       </varlistentry>
     </variablelist>