+++ /dev/null
-<?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" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><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"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="idm2123"></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 class="variablelist"><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="idm2170"></a><p class="title"><strong>Table 5.11. interpretation_argument</strong></p><div class="table-contents"><table class="table" summary="interpretation_argument" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px 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="idm2185"></a><p class="title"><strong>Table 5.12. interpretation_rhs</strong></p><div class="table-contents"><table class="table" summary="interpretation_rhs" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px 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>
\ No newline at end of file
projects / helm.git / blobdiff