From 275a432d33c455d75725d5991e82b62e7d01f68d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 18 Jun 2008 22:55:35 +0000
Subject: [PATCH] interpretation documented

---
 helm/software/matita/help/C/matita.xml        |   3 +
 helm/software/matita/help/C/sec_tactics.xml   |   2 +-
 helm/software/matita/help/C/sec_terms.xml     |  12 ++
 .../matita/help/C/sec_usernotation.xml        | 108 ++++++++++++++++--
 4 files changed, 115 insertions(+), 10 deletions(-)

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 3f00c148f..cb94d108c 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -55,6 +55,9 @@
   <!ENTITY autoparams "<emphasis><link linkend='grammar.autoparams'>auto_params</link></emphasis>">
   <!ENTITY justification "<emphasis><link linkend='grammar.justification'>justification</link></emphasis>">
   <!ENTITY simpleautoparam "<emphasis><link linkend='grammar.simpleautoparam'>simple_auto_param</link></emphasis>">
+  <!ENTITY interpretation_argument "<emphasis><link linkend='grammar.interpretation_argument'>interpretation_argument</link></emphasis>">
+  <!ENTITY interpretation_rhs "<emphasis><link linkend='grammar.interpretation_rhs'>interpretation_rhs</link></emphasis>">
+  <!ENTITY csymbol "<emphasis><link linkend='grammar.csymbol'>csymbol</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index b98570407..0205ce8a8 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -61,7 +61,7 @@
           <term>Pre-conditions:</term>
           <listitem>
             <para><command>t</command> must have type
-             <command>T<subscript>1</subscript> → ... →
+             <command>T<subscript>1</subscript> → … →
               T<subscript>n</subscript> → G</command>
              where <command>G</command> can be unified with the conclusion
              of the current sequent.</para>
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index bff00d6f2..082a5bb75 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -98,6 +98,18 @@
       </tbody>
      </tgroup>
     </table>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>csymbol</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.csymbol">&csymbol;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">'</emphasis>&id;</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index 147edc084..f4b3cc411 100644
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -2,17 +2,107 @@
 <!-- ============ User Notation ====================== -->
 <chapter id="sec_usernotation">
  <title>Extending the syntax</title>
+  Introduction: TODO
  <sect1>
-   <title>Introduction</title>
-   <para>
-     &TODO;
-   </para>
-   <para id="notation">
-     notation: &TODO;
-   </para>
+  <title>notation</title>
+  <titleabbrev>notation</titleabbrev>
+  <para id="notation">
+    notation: &TODO;
+  </para>
+ </sect1>
+ <sect1>
+   <title>interpretation</title>
+   <titleabbrev>interpretation</titleabbrev>
+   <para><userinput>interpretation &quot;description&quot; 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
+         rhs</userinput></para>
    <para id="interpretation">
-     interpretation: &TODO;
+    <variablelist>
+      <varlistentry role="tactic.synopsis">
+        <term>Synopsis:</term>
+        <listitem>
+          <para><emphasis role="bold">interpretation</emphasis>
+           &qstring; &csymbol; [&interpretation_argument;]…
+           <emphasis role="bol">=</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 &quot;η&quot;, 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>
-
-- 
2.39.2