helm/software/matita/help/C/sec_usernotation.xml

   1
   2 <!-- ============ User Notation ====================== -->
   3 <chapter id="sec_usernotation">
   4  <title>Extending the syntax</title>
   5   Introduction: TODO
   6  <sect1>
   7   <title>notation</title>
   8   <titleabbrev>notation</titleabbrev>
   9   <para id="notation">
  10     notation: &TODO;
  11   </para>
  12  </sect1>
  13  <sect1>
  14    <title>interpretation</title>
  15    <titleabbrev>interpretation</titleabbrev>
  16    <para><userinput>interpretation &quot;description&quot; 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
  17          rhs</userinput></para>
  18    <para id="interpretation">
  19     <variablelist>
  20       <varlistentry role="tactic.synopsis">
  21         <term>Synopsis:</term>
  22         <listitem>
  23           <para><emphasis role="bold">interpretation</emphasis>
  24            &qstring; &csymbol; [&interpretation_argument;]…
  25            <emphasis role="bol">=</emphasis>
  26            &interpretation_rhs;
  27           </para>
  28         </listitem>
  29       </varlistentry>
  30       <varlistentry>
  31        <term>Action:</term>
  32        <listitem>
  33          <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>
  34           (the simultaneous substitution in <command>rhs</command> of the
  35           interpretation <command>{…}</command> of every content-level
  36           actual argument <command>t<subscript>i</subscript></command> for its
  37           corresponding formal parameter
  38           <command>p<subscript>i</subscript></command>). The
  39           <command>description</command> must be a textual description of the
  40           meaning associated to <command>'symbol</command> by this
  41           interpretation, and is used by the user interface of Matita to
  42           provide feedback on the interpretation of ambiguous terms.
  43          </para>
  44        </listitem>
  45       </varlistentry>
  46       <varlistentry>
  47         <term>Interpretation arguments:</term>
  48         <listitem>
  49
  50     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  51       <title>interpretation_argument</title>
  52       <tgroup cols="4">
  53       <tbody>
  54        <row>
  55         <entry id="grammar.interpretation_argument">&interpretation_argument;</entry>
  56         <entry>::=</entry>
  57         <entry>[<emphasis role="bold">η</emphasis><emphasis role="bold">.</emphasis>]… &id;</entry>
  58         <entry>A formal parameter. If the name of the formal parameter is
  59          prefixed by n symbols &quot;η&quot;, then the mapping performs
  60          (multiple) η-expansions to grant that the semantic actual
  61          parameter begins with at least n λ-abstractions.</entry>
  62        </row>
  63       </tbody>
  64       </tgroup>
  65      </table>
  66     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  67       <title>interpretation_rhs</title>
  68       <tgroup cols="4">
  69       <tbody>
  70        <row>
  71         <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
  72         <entry>::=</entry>
  73         <entry>&uri;</entry>
  74         <entry>A constant, specified by its URI</entry>
  75        </row>
  76        <row>
  77         <entry></entry>
  78         <entry>|</entry>
  79         <entry>&id;</entry>
  80         <entry>A constant, specified by its name, or a bound variable. If
  81                the constant name is ambiguous, the one corresponding to the
  82                last implicitly or explicitly specified alias is used.</entry>
  83        </row>
  84        <row>
  85         <entry></entry>
  86         <entry>|</entry>
  87         <entry><emphasis role="bold">_</emphasis></entry>
  88         <entry>An implicit parameter</entry>
  89        </row>
  90        <row>
  91         <entry></entry>
  92         <entry>|</entry>
  93         <entry><emphasis role="bold">(</emphasis>
  94                &interpretation_rhs;
  95                [&interpretation_rhs;]…
  96                <emphasis role="bold">)</emphasis></entry>
  97         <entry>An application</entry>
  98        </row>
  99       </tbody>
 100       </tgroup>
 101      </table>
 102
 103         </listitem>
 104       </varlistentry>
 105     </variablelist>
 106    </para>
 107  </sect1>
 108 </chapter>