2 <!-- ============ Commands ====================== -->
3 <chapter id="sec_commands">
4 <title>Other commands</title>
5 <sect1 id="command_alias">
7 <para><userinput>alias id "s" = "def"</userinput></para>
8 <para><userinput>alias symbol "s" (instance n) = "def"</userinput></para>
9 <para><userinput>alias num (instance n) = "def"</userinput></para>
12 <varlistentry role="tactic.synopsis">
13 <term>Synopsis:</term>
15 <para><emphasis role="bold">alias</emphasis>
16 [<emphasis role="bold">id</emphasis> &qstring; <emphasis role="bold">=</emphasis> &qstring;
17 | <emphasis role="bold">symbol</emphasis> &qstring; [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> &qstring;
18 | <emphasis role="bold">num</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> &qstring;
26 <para>Used to give an hint to the disambiguating parser.
27 When the parser is faced to the identifier (or symbol)
28 <command>s</command> or to any number, it will prefer
29 interpretations that "map <command>s</command> (or the
30 number) to <command>def</command>". For identifiers,
31 "def" is the URI of the interpretation.
32 E.g.: <command>cic:/matita/nat/nat.ind#xpointer(1/1/1)</command>
33 for the first constructor of the first inductive type defined
34 in the block of inductive type(s)
35 <command>cic:/matita/nat/nat.ind</command>.
36 For symbols and numbers, "def" is the label used to
38 <link linkend="interpretation">interpretation</link>.
40 <para>When a symbol or a number occurs several times in the
41 term to be parsed, it is possible to give an hint only for the
42 instance <command>n</command>. When the instance is omitted,
43 the hint is valid for every occurrence.
46 Hints are automatically inserted in the script by Matita every
47 time the user is interactively asked a question to disambiguate
48 a term. This way the user won't be posed the same question twice
49 when the script will be executed again.</para>
55 <sect1 id="command_check">
57 <para><userinput>check t</userinput></para>
60 <varlistentry role="tactic.synopsis">
61 <term>Synopsis:</term>
63 <para><emphasis role="bold">check</emphasis> &term;</para>
69 <para>Opens a CIC browser window that shows <command>t</command>
70 together with its type. The command is immediately removed from
77 <sect1 id="command_coercion">
78 <title>coercion</title>
79 <para><userinput>coercion u</userinput></para>
82 <varlistentry role="tactic.synopsis">
83 <term>Synopsis:</term>
85 <para><emphasis role="bold">coercion</emphasis> &uri;</para>
91 <para>Declares <command>u</command> as an implicit coercion
92 from the type of its last argument (source)
93 to its codomain (target). Every time a term <command>x</command>
94 of type source is used with expected type target, Matita
95 automatically replaces <command>x</command> with
96 <command>(u ? … ? x)</command> to avoid a typing error.</para>
97 <para>Implicit coercions are not displayed to the user:
98 <command>(u ? … ? x)</command> is rendered simply
99 as <command>x</command>.</para>
100 <para>When a coercion <command>u</command> is declared
101 from source <command>s</command> to target <command>t</command>
102 and there is already a coercion <command>u'</command> of
103 target <command>s</command> or source <command>t</command>,
104 a composite implicit coercion is automatically computed
111 <sect1 id="command_default">
112 <title>default</title>
113 <para><userinput></userinput></para>
116 <varlistentry role="tactic.synopsis">
117 <term>Synopsis:</term>
119 <para><emphasis role="bold">default</emphasis>
132 <sect1 id="command_hint">
134 <para><userinput>hint</userinput></para>
137 <varlistentry role="tactic.synopsis">
138 <term>Synopsis:</term>
140 <para><emphasis role="bold">hint</emphasis>
147 <para>Displays a list of theorems that can be successfully
148 applied to the current selected sequent. The command is
149 removed from the script, but the window that displays the
150 theorems allow to add to the script the application of the
158 <sect1 id="command_include">
159 <title>include</title>
160 <para><userinput>include "s"</userinput></para>
163 <varlistentry role="tactic.synopsis">
164 <term>Synopsis:</term>
166 <para><emphasis role="bold">include</emphasis> &qstring;</para>
172 <para>Every <link linkend="command_coercion">coercion</link>,
173 <link linkend="notation">notation</link> and
174 <link linkend="interpretation">interpretation</link> that was active
175 when the file <command>s</command> was compiled last time
176 is made active. The same happens for declarations of
177 <link linkend="command_default">default definitions and
178 theorems</link> and disambiguation
179 hints (<link linkend="command_alias">aliases</link>).
180 On the contrary, theorem and definitions declared in a file can be
181 immediately used without including it.</para>
182 <para>The file <command>s</command> is automatically compiled
183 if it is not compiled yet and if it is handled by a
184 <link linkend="developments">development</link>.
191 <sect1 id="command_include_first">
192 <title>include' "s"</title>
193 <para><userinput></userinput></para>
196 <varlistentry role="tactic.synopsis">
197 <term>Synopsis:</term>
199 <para><emphasis role="bold">include'</emphasis> &qstring;</para>
205 <para>Not documented (&TODO;), do not use it.</para>
211 <sect1 id="command_set">
213 <para><userinput>set "baseuri" "s"</userinput></para>
216 <varlistentry role="tactic.synopsis">
217 <term>Synopsis:</term>
219 <para><emphasis role="bold">set</emphasis> &qstring; &qstring;</para>
225 <para>Sets to <command>s</command> the baseuri of all the
226 theorems and definitions stated in the current file.
227 The baseuri should be <command>a/b/c/foo</command>
228 if the file is named <command>foo</command> and it is in
229 the subtree <command>a/b/c</command> of the current
230 <link linkend="developments">development</link>.
231 This requirement is not enforced, but it could be in the future.
233 <para>Currently, <command>baseuri</command> is the only
234 property that can be set even if the parser accepts
235 arbitrary property names.</para>
241 <sect1 id="command_whelp">
243 <para><userinput></userinput></para>
246 <varlistentry role="tactic.synopsis">
247 <term>Synopsis:</term>
249 <para><emphasis role="bold">whelp</emphasis>
262 <sect1 id="command_qed">
264 <para><userinput></userinput></para>
267 <varlistentry role="tactic.synopsis">
268 <term>Synopsis:</term>
270 <para><emphasis role="bold">qed</emphasis>
277 <para>Saves and indexes the current interactive theorem or
279 In order to do this, the set of sequents still to be proved
280 must be empty.</para>