/usr/share/doc/matita-doc/html/ch05s02.html is in matita-doc 0.5.8-3build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 | <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>interpretation</title><link rel="stylesheet" href="docbook.css" type="text/css" /><meta name="generator" content="DocBook XSL Stylesheets V1.75.2" /><link rel="home" href="index.html" title="Matita V0.5.8 User Manual (rev. 0.5.8 )" /><link rel="up" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /><link rel="prev" href="sec_usernotation.html" title="Chapter 5. Extending the syntax" /><link rel="next" href="sec_tacticals.html" title="Chapter 6. Tacticals" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">interpretation</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="sec_usernotation.html">Prev</a> </td><th width="60%" align="center">Chapter 5. Extending the syntax</th><td width="20%" align="right"> <a accesskey="n" href="sec_tacticals.html">Next</a></td></tr></table><hr /></div><div class="sect1" title="interpretation"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="idp3900720"></a>interpretation</h2></div></div></div><p><strong class="userinput"><code>interpretation "description" 'symbol p<sub>1</sub> … p<sub>n</sub> =
rhs</code></strong></p><p><a id="interpretation"></a>
</p><div class="variablelist"><dl><dt><span class="term">Synopsis:</span></dt><dd><p><span class="bold"><strong>interpretation</strong></span>
<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.csymbol">csymbol</a></em></span> [<span class="emphasis"><em><a class="link" href="ch05s02.html#grammar.interpretation_argument">interpretation_argument</a></em></span>]…
<span class="bold"><strong>=</strong></span>
<span class="emphasis"><em><a class="link" href="ch05s02.html#grammar.interpretation_rhs">interpretation_rhs</a></em></span>
</p></dd><dt><span class="term">Action:</span></dt><dd><p>It declares a bi-directional mapping <span class="command"><strong>{…}</strong></span> between the content-level AST <span class="command"><strong>'symbol t<sub>1</sub> … t<sub>n</sub></strong></span> and the semantic term <span class="command"><strong>rhs[{t<sub>1</sub>}/p<sub>1</sub>;…;{t<sub>n</sub>}/p<sub>n</sub>]</strong></span>
(the simultaneous substitution in <span class="command"><strong>rhs</strong></span> of the
interpretation <span class="command"><strong>{…}</strong></span> of every content-level
actual argument <span class="command"><strong>t<sub>i</sub></strong></span> for its
corresponding formal parameter
<span class="command"><strong>p<sub>i</sub></strong></span>). The
<span class="command"><strong>description</strong></span> must be a textual description of the
meaning associated to <span class="command"><strong>'symbol</strong></span> by this
interpretation, and is used by the user interface of Matita to
provide feedback on the interpretation of ambiguous terms.
</p></dd><dt><span class="term">Interpretation arguments:</span></dt><dd><div class="table"><a id="idp3912504"></a><p class="title"><b>Table 5.11. interpretation_argument</b></p><div class="table-contents"><table summary="interpretation_argument" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.interpretation_argument"></a><span class="emphasis"><em><a class="link" href="ch05s02.html#grammar.interpretation_argument">interpretation_argument</a></em></span></td><td style="">::=</td><td style="">[<span class="bold"><strong>η</strong></span><span class="bold"><strong>.</strong></span>]… <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style="">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.</td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp3917080"></a><p class="title"><b>Table 5.12. interpretation_rhs</b></p><div class="table-contents"><table summary="interpretation_rhs" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.interpretation_rhs"></a><span class="emphasis"><em><a class="link" href="ch05s02.html#grammar.interpretation_rhs">interpretation_rhs</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.uri">uri</a></em></span></td><td style="">A constant, specified by its URI</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.id">id</a></em></span></td><td style="">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.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>?</strong></span></td><td style="">An implicit parameter</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>(</strong></span>
<span class="emphasis"><em><a class="link" href="ch05s02.html#grammar.interpretation_rhs">interpretation_rhs</a></em></span>
[<span class="emphasis"><em><a class="link" href="ch05s02.html#grammar.interpretation_rhs">interpretation_rhs</a></em></span>]…
<span class="bold"><strong>)</strong></span></td><td style="">An application</td></tr></tbody></table></div></div><br class="table-break" /></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="sec_usernotation.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_usernotation.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_tacticals.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 5. Extending the syntax </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 6. Tacticals</td></tr></table></div></body></html>
|