2 <!-- ============ User Notation ====================== -->
3 <chapter id="sec_usernotation">
4 <title>Extending the syntax</title>
7 <title>notation</title>
8 <titleabbrev>notation</titleabbrev>
14 <title>interpretation</title>
15 <titleabbrev>interpretation</titleabbrev>
16 <para><userinput>interpretation "description" 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
17 rhs</userinput></para>
18 <para id="interpretation">
20 <varlistentry role="tactic.synopsis">
21 <term>Synopsis:</term>
23 <para><emphasis role="bold">interpretation</emphasis>
24 &qstring; &csymbol; [&interpretation_argument;]…
25 <emphasis role="bol">=</emphasis>
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.
47 <term>Interpretation arguments:</term>
50 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
51 <title>interpretation_argument</title>
55 <entry id="grammar.interpretation_argument">&interpretation_argument;</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 "η", then the mapping performs
60 (multiple) η-expansions to grant that the semantic actual
61 parameter begins with at least n λ-abstractions.</entry>
66 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
67 <title>interpretation_rhs</title>
71 <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
74 <entry>A constant, specified by its URI</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>
87 <entry><emphasis role="bold">_</emphasis></entry>
88 <entry>An implicit parameter</entry>
93 <entry><emphasis role="bold">(</emphasis>
95 [&interpretation_rhs;]…
96 <emphasis role="bold">)</emphasis></entry>
97 <entry>An application</entry>