]> matita.cs.unibo.it Git - helm.git/blob - matita/help/C/sec_commands.xml
- added some aliases
[helm.git] / matita / help / C / sec_commands.xml
1
2 <!-- ============ Commands ====================== -->
3 <chapter id="sec_commands">
4  <title>Other commands</title>
5  <sect1 id="command_alias">
6    <title>alias</title>
7    <para><userinput>alias id &quot;s&quot; = &quot;def&quot;</userinput></para>
8    <para><userinput>alias symbol &quot;s&quot; (instance n) = &quot;def&quot;</userinput></para>
9    <para><userinput>alias num (instance n) = &quot;def&quot;</userinput></para>
10    <para>
11      <variablelist>
12        <varlistentry>
13          <term>Synopsis:</term>
14          <listitem>
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;
19             ]
20            </para>
21          </listitem>
22        </varlistentry>
23        <varlistentry>
24          <term>Action:</term>
25          <listitem>
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 &quot;map <command>s</command> (or the
30             number) to <command>def</command>&quot;. For identifiers,
31             &quot;def&quot; 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, &quot;def&quot; is the label used to
37             mark the wanted
38             <link linkend="interpretation">interpretation</link>.
39            </para>
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.
44           </para>
45           <para>
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>
50          </listitem>
51        </varlistentry>
52      </variablelist>
53    </para>
54  </sect1>
55  <sect1 id="command_check">
56    <title>check</title>
57    <para><userinput>check t</userinput></para>
58    <para>
59      <variablelist>
60        <varlistentry>
61          <term>Synopsis:</term>
62          <listitem>
63            <para><emphasis role="bold">check</emphasis> &term;</para>
64          </listitem>
65        </varlistentry>
66        <varlistentry>
67          <term>Action:</term>
68          <listitem>
69            <para>Opens a CIC browser window that shows <command>t</command>
70             together with its type. The command is immediately removed from
71             the script.</para>
72          </listitem>
73        </varlistentry>
74      </variablelist>
75    </para>
76  </sect1>
77  <sect1 id="command_coercion">
78    <title>coercion</title>
79    <para><userinput>coercion u</userinput></para>
80    <para>
81      <variablelist>
82        <varlistentry>
83          <term>Synopsis:</term>
84          <listitem>
85            <para><emphasis role="bold">coercion</emphasis> &uri;</para>
86          </listitem>
87        </varlistentry>
88        <varlistentry>
89          <term>Action:</term>
90          <listitem>
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
105             by Matita.</para>
106          </listitem>
107        </varlistentry>
108      </variablelist>
109    </para>
110  </sect1>
111  <sect1 id="command_default">
112    <title>default</title>
113    <para><userinput>default &quot;s&quot; u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
114    <para>
115      <variablelist>
116        <varlistentry>
117          <term>Synopsis:</term>
118          <listitem>
119            <para><emphasis role="bold">default</emphasis>
120             &qstring; &uri; [&uri;]…
121            </para>
122          </listitem>
123        </varlistentry>
124        <varlistentry>
125          <term>Action:</term>
126          <listitem>
127            <para>It registers a cluster of related definitions and
128             theorems to be used by tactics and the rendering engine.
129             Some functionalities of Matita are not available when some
130             clusters have not been registered. Overloading a cluster
131             registration is possible: the last registration will be the
132             default one, but the previous ones are still in effect.</para>
133            <para>
134             <command>s</command> is an identifier of the cluster and
135             <command>u<subscript>1</subscript> … u<subscript>n</subscript></command>
136             are the URIs of the definitions and theorems of the cluster.
137             The number <command>n</command> of required URIs depends on the
138             cluster. The following clusters are supported.
139            </para>
140            <table>
141             <title>clusters</title>
142             <tgroup cols="6">
143             <thead>
144              <row>
145               <entry>name</entry>
146               <entry>expected object for 1st URI</entry>
147               <entry>expected object for 2nd URI</entry>
148               <entry>expected object for 3rd URI</entry>
149               <entry>expected object for 4th URI</entry>
150               <entry>expected object for 5th URI</entry>
151              </row>
152             </thead>
153             <tbody>
154              <row>
155               <entry>equality</entry>
156               <entry>an inductive type (say, of type <command>eq</command>) of type ∀A:Type.A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis> with one family parameter and one constructor of type ∀x:A.eq A x</entry>
157               <entry>a theorem of type <emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq A y x</entry>
158               <entry>a theorem of type <emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>x,y,z:A.eq A x y <emphasis role="bold">→</emphasis> eq A y z <emphasis role="bold">→</emphasis> eq A x z</entry>
159               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
160               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Prop</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
161              </row>
162              <row>
163               <entry>true</entry>
164               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> with only one constructor that has no arguments</entry>
165               <entry/>
166               <entry/>
167               <entry/>
168               <entry/>
169              </row>
170              <row>
171               <entry>false</entry>
172               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> without constructors</entry>
173               <entry/>
174               <entry/>
175               <entry/>
176               <entry/>
177              </row>
178              <row>
179               <entry>absurd</entry>
180               <entry>a theorem of type <emphasis role="bold">∀</emphasis>A:Prop.<emphasis role="bold">∀</emphasis>B:Prop.A <emphasis role="bold">→</emphasis> Not A <emphasis role="bold">→</emphasis> B</entry>
181               <entry/>
182               <entry/>
183               <entry/>
184               <entry/>
185              </row>
186             </tbody>
187             </tgroup>
188            </table>
189          </listitem>
190        </varlistentry>
191      </variablelist>
192    </para>
193  </sect1>
194  <sect1 id="command_hint">
195    <title>hint</title>
196    <para><userinput>hint</userinput></para>
197    <para>
198      <variablelist>
199        <varlistentry>
200          <term>Synopsis:</term>
201          <listitem>
202            <para><emphasis role="bold">hint</emphasis>
203            </para>
204          </listitem>
205        </varlistentry>
206        <varlistentry>
207          <term>Action:</term>
208          <listitem>
209            <para>Displays a list of theorems that can be successfully
210             applied to the current selected sequent. The command is
211             removed from the script, but the window that displays the
212             theorems allow to add to the script the application of the
213             selected theorem.
214            </para>
215          </listitem>
216        </varlistentry>
217      </variablelist>
218    </para>
219  </sect1>
220  <sect1 id="command_include">
221    <title>include</title>
222    <para><userinput>include &quot;s&quot;</userinput></para>
223    <para>
224      <variablelist>
225        <varlistentry>
226          <term>Synopsis:</term>
227          <listitem>
228            <para><emphasis role="bold">include</emphasis> &qstring;</para>
229          </listitem>
230        </varlistentry>
231        <varlistentry>
232          <term>Action:</term>
233          <listitem>
234            <para>Every <link linkend="command_coercion">coercion</link>,
235             <link linkend="notation">notation</link> and
236             <link linkend="interpretation">interpretation</link> that was active
237             when the file <command>s</command> was compiled last time
238             is made active. The same happens for declarations of
239             <link linkend="command_default">default definitions and
240             theorems</link> and disambiguation
241             hints (<link linkend="command_alias">aliases</link>).
242             On the contrary, theorem and definitions declared in a file can be
243            immediately used without including it.</para>
244           <para>The file <command>s</command> is automatically compiled
245            if it is not compiled yet and if it is handled by a
246            <link linkend="developments">development</link>.
247           </para>
248          </listitem>
249        </varlistentry>
250      </variablelist>
251    </para>
252  </sect1>
253  <sect1 id="command_include_first">
254    <title>include' &quot;s&quot;</title>
255    <para><userinput></userinput></para>
256    <para>
257      <variablelist>
258        <varlistentry>
259          <term>Synopsis:</term>
260          <listitem>
261            <para><emphasis role="bold">include'</emphasis> &qstring;</para>
262          </listitem>
263        </varlistentry>
264        <varlistentry>
265          <term>Action:</term>
266          <listitem>
267            <para>Not documented (&TODO;), do not use it.</para>
268          </listitem>
269        </varlistentry>
270      </variablelist>
271    </para>
272  </sect1>
273  <sect1 id="command_set">
274    <title>set</title>
275    <para><userinput>set &quot;baseuri&quot; &quot;s&quot;</userinput></para>
276    <para>
277      <variablelist>
278        <varlistentry>
279          <term>Synopsis:</term>
280          <listitem>
281            <para><emphasis role="bold">set</emphasis> &qstring; &qstring;</para>
282          </listitem>
283        </varlistentry>
284        <varlistentry>
285          <term>Action:</term>
286          <listitem>
287            <para>Sets to <command>s</command> the baseuri of all the
288             theorems and definitions stated in the current file.
289             The baseuri should be <command>a/b/c/foo</command>
290             if the file is named <command>foo</command> and it is in
291             the subtree <command>a/b/c</command> of the current
292             <link linkend="developments">development</link>.
293             This requirement is not enforced, but it could be in the future.
294            </para>
295            <para>Currently, <command>baseuri</command> is the only
296             property that can be set even if the parser accepts
297             arbitrary property names.</para>
298          </listitem>
299        </varlistentry>
300      </variablelist>
301    </para>
302  </sect1>
303  <sect1 id="command_whelp">
304    <title>whelp</title>
305    <para><userinput>whelp locate &quot;s&quot;</userinput></para>
306    <para><userinput>whelp hint t</userinput></para>
307    <para><userinput>whelp elim t</userinput></para>
308    <para><userinput>whelp match t</userinput></para>
309    <para><userinput>whelp instance t</userinput></para>
310    <para>
311      <variablelist>
312        <varlistentry>
313          <term>Synopsis:</term>
314          <listitem>
315            <para><emphasis role="bold">whelp</emphasis>
316             [<emphasis role="bold">locate</emphasis> &qstring;
317             | <emphasis role="bold">hint</emphasis> &term;
318             | <emphasis role="bold">elim</emphasis> &term;
319             | <emphasis role="bold">match</emphasis> &term;
320             | <emphasis role="bold">instance</emphasis> &term;
321             ]
322            </para>
323          </listitem>
324        </varlistentry>
325        <varlistentry>
326          <term>Action:</term>
327          <listitem>
328            <para>Performs the corresponding <link linkend="whelp">query</link>,
329             showing the result in the CIC browser. The command is removed
330             from the script.
331            </para>
332          </listitem>
333        </varlistentry>
334      </variablelist>
335    </para>
336  </sect1>
337  <sect1 id="command_qed">
338    <title>qed</title>
339    <para><userinput></userinput></para>
340    <para>
341      <variablelist>
342        <varlistentry>
343          <term>Synopsis:</term>
344          <listitem>
345            <para><emphasis role="bold">qed</emphasis>
346            </para>
347          </listitem>
348        </varlistentry>
349        <varlistentry>
350          <term>Action:</term>
351          <listitem>
352            <para>Saves and indexes the current interactive theorem or
353             definition.
354             In order to do this, the set of sequents still to be proved
355             must be empty.</para>
356          </listitem>
357        </varlistentry>
358      </variablelist>
359    </para>
360  </sect1>
361 </chapter>
362