1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
2 <!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>Chapter 9. Other commands</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="prev" href="tac_bytermweproved.html" title="we proved" /><link rel="next" href="command_check.html" title="check" /></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">Chapter 9. Other commands</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_bytermweproved.html">Prev</a> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="command_check.html">Next</a></td></tr></table><hr /></div><div class="chapter"><div class="titlepage"><div><div><h1 class="title"><a id="sec_commands"></a>Chapter 9. Other commands</h1></div></div></div><div class="toc"><p><strong>Table of Contents</strong></p><dl class="toc"><dt><span class="sect1"><a href="sec_commands.html#command_alias">alias</a></span></dt><dt><span class="sect1"><a href="command_check.html">check</a></span></dt><dt><span class="sect1"><a href="command_eval.html">eval</a></span></dt><dt><span class="sect1"><a href="command_prefer_coercion.html">prefer coercion</a></span></dt><dt><span class="sect1"><a href="command_coercion.html">coercion</a></span></dt><dt><span class="sect1"><a href="command_default.html">default</a></span></dt><dt><span class="sect1"><a href="command_hint.html">hint</a></span></dt><dt><span class="sect1"><a href="command_include.html">include</a></span></dt><dt><span class="sect1"><a href="command_include_first.html">include' "s"</a></span></dt><dt><span class="sect1"><a href="command_whelp.html">whelp</a></span></dt><dt><span class="sect1"><a href="command_qed.html">qed</a></span></dt><dt><span class="sect1"><a href="command_inline.html">inline</a></span></dt><dd><dl><dt><span class="sect2"><a href="command_inline.html#inline-params">inline-params</a></span></dt></dl></dd></dl></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="command_alias"></a>alias</h2></div></div></div><p><strong class="userinput"><code>alias id "s" = "def"</code></strong></p><p><strong class="userinput"><code>alias symbol "s" (instance n) = "def"</code></strong></p><p><strong class="userinput"><code>alias num (instance n) = "def"</code></strong></p><p>
3 </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p><span class="bold"><strong>alias</strong></span>
4 [<span class="bold"><strong>id</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span> <span class="bold"><strong>=</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span>
5 | <span class="bold"><strong>symbol</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span> [<span class="bold"><strong>(instance</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span><span class="bold"><strong>)</strong></span>] <span class="bold"><strong>=</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span>
6 | <span class="bold"><strong>num</strong></span> [<span class="bold"><strong>(instance</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span><span class="bold"><strong>)</strong></span>] <span class="bold"><strong>=</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span>
8 </p></dd><dt><span class="term">Action:</span></dt><dd><p>Used to give an hint to the disambiguating parser.
9 When the parser is faced to the identifier (or symbol)
10 <span class="command"><strong>s</strong></span> or to any number, it will prefer
11 interpretations that "map <span class="command"><strong>s</strong></span> (or the
12 number) to <span class="command"><strong>def</strong></span>". For identifiers,
13 "def" is the URI of the interpretation.
14 E.g.: <span class="command"><strong>cic:/matita/nat/nat.ind#xpointer(1/1/1)</strong></span>
15 for the first constructor of the first inductive type defined
16 in the block of inductive type(s)
17 <span class="command"><strong>cic:/matita/nat/nat.ind</strong></span>.
18 For symbols and numbers, "def" is the label used to
20 <a class="link" href="ch05s02.html#interpretation">interpretation</a>.
21 </p><p>When a symbol or a number occurs several times in the
22 term to be parsed, it is possible to give an hint only for the
23 instance <span class="command"><strong>n</strong></span>. When the instance is omitted,
24 the hint is valid for every occurrence.
26 Hints are automatically inserted in the script by Matita every
27 time the user is interactively asked a question to disambiguate
28 a term. This way the user won't be posed the same question twice
29 when the script will be executed again.</p></dd></dl></div><p>
30 </p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_bytermweproved.html">Prev</a> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="command_check.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">we proved </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> check</td></tr></table></div></body></html>