+ <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">¬ation_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>&layout; <emphasis role="bold">\frac</emphasis> &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">'</emphasis>&id;<emphasis role="bold">'</emphasis></entry>
+ <entry>New keyword for the lexer</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1>
+ <title>interpretation</title>
+ <titleabbrev>interpretation</titleabbrev>
+ <para><userinput>interpretation "description" 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
+ rhs</userinput></para>
+ <para id="interpretation">
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">interpretation</emphasis>
+ &qstring; &csymbol; [&interpretation_argument;]…
+ <emphasis role="bold">=</emphasis>
+ &interpretation_rhs;
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It declares a bi-directional mapping <command>{…}</command> between the content-level AST <command>'symbol t<subscript>1</subscript> … t<subscript>n</subscript></command> and the semantic term <command>rhs[{t<subscript>1</subscript>}/p<subscript>1</subscript>;…;{t<subscript>n</subscript>}/p<subscript>n</subscript>]</command>
+ (the simultaneous substitution in <command>rhs</command> of the
+ interpretation <command>{…}</command> of every content-level
+ actual argument <command>t<subscript>i</subscript></command> for its
+ corresponding formal parameter
+ <command>p<subscript>i</subscript></command>). The
+ <command>description</command> must be a textual description of the
+ meaning associated to <command>'symbol</command> by this
+ interpretation, and is used by the user interface of Matita to
+ provide feedback on the interpretation of ambiguous terms.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Interpretation arguments:</term>
+ <listitem>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>interpretation_argument</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.interpretation_argument">&interpretation_argument;</entry>
+ <entry>::=</entry>
+ <entry>[<emphasis role="bold">η</emphasis><emphasis role="bold">.</emphasis>]… &id;</entry>
+ <entry>A formal parameter. If the name of the formal parameter is
+ prefixed by n symbols "η", then the mapping performs
+ (multiple) η-expansions to grant that the semantic actual
+ parameter begins with at least n λ-abstractions.</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>interpretation_rhs</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
+ <entry>::=</entry>
+ <entry>&uri;</entry>
+ <entry>A constant, specified by its URI</entry>
+ </row>
+ <row>
+ <entry></entry>
+ <entry>|</entry>
+ <entry>&id;</entry>
+ <entry>A constant, specified by its name, or a bound variable. If
+ the constant name is ambiguous, the one corresponding to the
+ last implicitly or explicitly specified alias is used.</entry>
+ </row>
+ <row>
+ <entry></entry>
+ <entry>|</entry>
+ <entry><emphasis role="bold">_</emphasis></entry>
+ <entry>An implicit parameter</entry>
+ </row>
+ <row>
+ <entry></entry>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>
+ &interpretation_rhs;
+ [&interpretation_rhs;]…
+ <emphasis role="bold">)</emphasis></entry>
+ <entry>An application</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+</chapter>