matita/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> &sterm;</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  <!--
  78  <sect1 id="command_eval">
  79    <title>eval</title>
  80    <para><userinput>eval red on t</userinput></para>
  81    <para>
  82      <variablelist>
  83        <varlistentry>
  84          <term>Synopsis:</term>
  85          <listitem>
  86            <para><emphasis role="bold">eval</emphasis>
  87             &reduction-kind;
  88              <emphasis role="bold">on</emphasis>
  89              &term;</para>
  90          </listitem>
  91        </varlistentry>
  92        <varlistentry>
  93          <term>Action:</term>
  94          <listitem>
  95            <para>Opens a CIC browser window that shows
  96              the reduct of
  97              <command>t</command>
  98              together with its type.</para>
  99          </listitem>
 100        </varlistentry>
 101      </variablelist>
 102    </para>
 103  </sect1>
 104  -->
 105  <!--
 106  <sect1 id="command_prefer_coercion">
 107    <title>prefer coercion</title>
 108    <para><userinput>prefer coercion u</userinput></para>
 109    <para>
 110      <variablelist>
 111        <varlistentry>
 112          <term>Synopsis:</term>
 113          <listitem>
 114                  <para>
 115                          <emphasis role="bold">prefer coercion</emphasis>
 116        (&uri; | &term;)
 117                  </para>
 118          </listitem>
 119        </varlistentry>
 120        <varlistentry>
 121          <term>Action:</term>
 122          <listitem>
 123            <para>The already declared coercion <command>u</command>
 124              is preferred to other coercions with the same source and target.
 125            </para>
 126          </listitem>
 127        </varlistentry>
 128      </variablelist>
 129    </para>
 130  </sect1>
 131  -->
 132  <sect1 id="command_coercion">
 133    <title>coercion</title>
 134    <para><userinput>coercion nocomposites c : ty ≝ u on s : S to T</userinput></para>
 135    <para>
 136      <variablelist>
 137        <varlistentry>
 138          <term>Synopsis:</term>
 139          <listitem>
 140                  <para>
 141                          <emphasis role="bold">coercion</emphasis>
 142                          [ <emphasis role="bold">nocomposites</emphasis> ] &id;
 143                          [ :  &term; <emphasis role="bold">≝</emphasis> &term;
 144                               <emphasis role="bold">on</emphasis>
 145                               &id; : &term;
 146                               <emphasis role="bold">to</emphasis> &term; ]
 147                  </para>
 148          </listitem>
 149        </varlistentry>
 150        <varlistentry>
 151          <term>Action:</term>
 152          <listitem>
 153             <para>Declares <command>c</command> as an implicit coercion.
 154             If only <command>c</command> is given, <command>u</command>
 155             is the constant named by <command>c</command>,
 156             <command>ty</command> its declared type,
 157             <command>s</command> the name of the last variable abstracted in
 158             in <command>ty</command>, <command>S</command> the type of
 159             this last variable and <command>T</command> the target of
 160             <command>ty</command>. The user can specify all these component to
 161             have full control on how the coercion is indexed.
 162             The type of the body of the coercion <command>u</command> must be
 163             convertible to the declared one <command>ty</command>. Let it be
 164             <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command>.
 165             Then <command>s</command> must be one of <command>x1</command> …
 166             <command>xn</command> (possibly prefixed by <command>_</command>
 167             if the product is non dependent). Let <command>s</command>
 168             be <command>xi</command> in the following.
 169             Then <command>S</command> must be <command>Ti</command>
 170             where all bound variables are replaced by <command>?</command>,
 171             and <command>T</command> must be <command>Tn</command>
 172             where all bound variable are replaced by <command>?</command>.
 173             For example the following command
 174             declares a coercions from vectors of any length to lists of
 175             natural numbers.</para>
 176
 177             <para><userinput>coercion nocomposites v2l : ∀n:nat.∀v:Vect nat n.
 178             List nat ≝ l_of_v on _v : Vect nat ? to List nat</userinput></para>
 179
 180
 181             <para>Every time a term <command>x</command>
 182             of a type that matches <command>S</command>
 183                (<command>Vect nat ?</command> here)
 184                     is used with an expected
 185                     type that matches <command>T</command>
 186                     (<command>List nat</command> here), Matita
 187             automatically replaces <command>x</command> with
 188             <command>(u ? … ? x ? … ?)</command> to avoid a typing error.
 189             Note that the position of <command>x</command> is determined by
 190             <command>s</command>.</para>
 191
 192            <para>Implicit coercions are not displayed to the user:
 193             <command>(u ? … ? x)</command> is rendered simply
 194             as <command>x</command>.</para>
 195
 196            <para>When a coercion <command>u</command> is declared
 197             from source <command>s</command> to target <command>t</command>
 198             and there is already a coercion <command>u'</command> of
 199             target <command>s</command> or source <command>t</command>,
 200             a composite implicit coercion is automatically computed
 201             by Matita unless <emphasis role="bold">nocomposites</emphasis>
 202             is specified.</para>
 203
 204             <para>Note that <command>Vect nat ?</command> can be replaced with
 205             <command>Vect ? ?</command> to index the coercion is a loose way.</para>
 206          </listitem>
 207        </varlistentry>
 208      </variablelist>
 209    </para>
 210  </sect1>
 211  <!--
 212  <sect1 id="command_default">
 213    <title>default</title>
 214    <para><userinput>default &quot;s&quot; u<subscript>1</subscript> … u<subscript>n</subscript></userinput></para>
 215    <para>
 216      <variablelist>
 217        <varlistentry>
 218          <term>Synopsis:</term>
 219          <listitem>
 220            <para><emphasis role="bold">default</emphasis>
 221             &qstring; &uri; [&uri;]…
 222            </para>
 223          </listitem>
 224        </varlistentry>
 225        <varlistentry>
 226          <term>Action:</term>
 227          <listitem>
 228            <para>It registers a cluster of related definitions and
 229             theorems to be used by tactics and the rendering engine.
 230             Some functionalities of Matita are not available when some
 231             clusters have not been registered. Overloading a cluster
 232             registration is possible: the last registration will be the
 233             default one, but the previous ones are still in effect.</para>
 234            <para>
 235             <command>s</command> is an identifier of the cluster and
 236             <command>u<subscript>1</subscript> … u<subscript>n</subscript></command>
 237             are the URIs of the definitions and theorems of the cluster.
 238             The number <command>n</command> of required URIs depends on the
 239             cluster. The following clusters are supported.
 240            </para>
 241            <table>
 242             <title>clusters</title>
 243             <tgroup cols="6">
 244             <thead>
 245              <row>
 246               <entry>name</entry>
 247               <entry>expected object for 1st URI</entry>
 248               <entry>expected object for 2nd URI</entry>
 249               <entry>expected object for 3rd URI</entry>
 250               <entry>expected object for 4th URI</entry>
 251               <entry>expected object for 5th URI</entry>
 252               <entry>expected object for 6th URI</entry>
 253               <entry>expected object for 7th URI</entry>
 254               <entry>expected object for 8th URI</entry>
 255               <entry>expected object for 9th URI</entry>
 256               <entry>expected object for 10th URI</entry>
 257               <entry>expected object for 11th URI</entry>
 258              </row>
 259             </thead>
 260             <tbody>
 261              <row>
 262               <entry>equality</entry>
 263               <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>
 264               <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>
 265               <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>
 266               <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>
 267               <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>
 268               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Set</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
 269               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Set</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
 270               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Type</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A x y <emphasis role="bold">→</emphasis> P y</entry>
 271               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>a.<emphasis role="bold">∀</emphasis> P:A <emphasis role="bold">→</emphasis> <emphasis role="bold">Type</emphasis>.P x <emphasis role="bold">→</emphasis> <emphasis role="bold">∀</emphasis>y.eq A y x <emphasis role="bold">→</emphasis> P y</entry>
 272               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>B.<emphasis role="bold">∀</emphasis> f:A <emphasis role="bold">→</emphasis> B.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq B (f x) (f y)</entry>
 273               <entry><emphasis role="bold">∀</emphasis>A.<emphasis role="bold">∀</emphasis>B.<emphasis role="bold">∀</emphasis> f:A <emphasis role="bold">→</emphasis> B.<emphasis role="bold">∀</emphasis>x,y:A.eq A x y <emphasis role="bold">→</emphasis> eq B (f y) (f x)</entry>
 274              </row>
 275              <row>
 276               <entry>true</entry>
 277               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> with only one constructor that has no arguments</entry>
 278               <entry/>
 279               <entry/>
 280               <entry/>
 281               <entry/>
 282              </row>
 283              <row>
 284               <entry>false</entry>
 285               <entry>an inductive type of type <emphasis role="bold">Prop</emphasis> without constructors</entry>
 286               <entry/>
 287               <entry/>
 288               <entry/>
 289               <entry/>
 290              </row>
 291              <row>
 292               <entry>absurd</entry>
 293               <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>
 294               <entry/>
 295               <entry/>
 296               <entry/>
 297               <entry/>
 298              </row>
 299             </tbody>
 300             </tgroup>
 301            </table>
 302          </listitem>
 303        </varlistentry>
 304      </variablelist>
 305    </para>
 306  </sect1>
 307  -->
 308  <!--
 309  <sect1 id="command_hint">
 310    <title>hint</title>
 311    <para><userinput>hint</userinput></para>
 312    <para>
 313      <variablelist>
 314        <varlistentry>
 315          <term>Synopsis:</term>
 316          <listitem>
 317            <para><emphasis role="bold">hint</emphasis>
 318            </para>
 319          </listitem>
 320        </varlistentry>
 321        <varlistentry>
 322          <term>Action:</term>
 323          <listitem>
 324            <para>Displays a list of theorems that can be successfully
 325             applied to the current selected sequent. The command is
 326             removed from the script, but the window that displays the
 327             theorems allow to add to the script the application of the
 328             selected theorem.
 329            </para>
 330          </listitem>
 331        </varlistentry>
 332      </variablelist>
 333    </para>
 334  </sect1>
 335  -->
 336  <sect1 id="command_include">
 337    <title>include</title>
 338    <para><userinput>include &quot;s&quot;</userinput></para>
 339    <para>
 340      <variablelist>
 341        <varlistentry>
 342          <term>Synopsis:</term>
 343          <listitem>
 344            <para><emphasis role="bold">include</emphasis> &qstring;</para>
 345          </listitem>
 346        </varlistentry>
 347        <varlistentry>
 348          <term>Action:</term>
 349          <listitem>
 350            <para>Every <link linkend="command_coercion">coercion</link>,
 351             <link linkend="notation">notation</link> and
 352             <link linkend="interpretation">interpretation</link> that was active
 353             when the file <command>s</command> was compiled last time
 354             is made active. The same happens for declarations of
 355             <link linkend="command_default">default definitions and
 356             theorems</link> and disambiguation
 357             hints (<link linkend="command_alias">aliases</link>).
 358             On the contrary, theorem and definitions declared in a file can be
 359            immediately used without including it.</para>
 360            <para>The file <command>s</command> is automatically compiled
 361            if it is not compiled yet.
 362           </para>
 363           <para>
 364           If the file <command>s</command> was already included, either
 365           directly or recursively, the commands does nothing.
 366           </para>
 367          </listitem>
 368        </varlistentry>
 369      </variablelist>
 370    </para>
 371  </sect1>
 372  <sect1 id="command_include_alias">
 373    <title>include alias</title>
 374    <para><userinput>include alias &quot;s&quot;</userinput></para>
 375    <para>
 376      <variablelist>
 377        <varlistentry>
 378          <term>Synopsis:</term>
 379          <listitem>
 380            <para><emphasis role="bold">include</emphasis> <emphasis role="bold">alias</emphasis> &qstring;</para>
 381          </listitem>
 382        </varlistentry>
 383        <varlistentry>
 384          <term>Action:</term>
 385          <listitem>
 386            <para>Every
 387             <link linkend="interpretation">interpretation</link>
 388             declared in the file <command>s</command> is re-declared
 389             so to make it the preferred choice for disambiguation.
 390           </para>
 391          </listitem>
 392        </varlistentry>
 393      </variablelist>
 394    </para>
 395  </sect1>
 396  <!--
 397  <sect1 id="command_include_first">
 398    <title>include' &quot;s&quot;</title>
 399    <para><userinput></userinput></para>
 400    <para>
 401      <variablelist>
 402        <varlistentry>
 403          <term>Synopsis:</term>
 404          <listitem>
 405            <para><emphasis role="bold">include'</emphasis> &qstring;</para>
 406          </listitem>
 407        </varlistentry>
 408        <varlistentry>
 409          <term>Action:</term>
 410          <listitem>
 411            <para>Not documented (&TODO;), do not use it.</para>
 412          </listitem>
 413        </varlistentry>
 414      </variablelist>
 415    </para>
 416  </sect1>
 417  -->
 418  <!--
 419  <sect1 id="command_whelp">
 420    <title>whelp</title>
 421    <para><userinput>whelp locate &quot;s&quot;</userinput></para>
 422    <para><userinput>whelp hint t</userinput></para>
 423    <para><userinput>whelp elim t</userinput></para>
 424    <para><userinput>whelp match t</userinput></para>
 425    <para><userinput>whelp instance t</userinput></para>
 426    <para>
 427      <variablelist>
 428        <varlistentry>
 429          <term>Synopsis:</term>
 430          <listitem>
 431            <para><emphasis role="bold">whelp</emphasis>
 432             [<emphasis role="bold">locate</emphasis> &qstring;
 433             | <emphasis role="bold">hint</emphasis> &term;
 434             | <emphasis role="bold">elim</emphasis> &term;
 435             | <emphasis role="bold">match</emphasis> &term;
 436             | <emphasis role="bold">instance</emphasis> &term;
 437             ]
 438            </para>
 439          </listitem>
 440        </varlistentry>
 441        <varlistentry>
 442          <term>Action:</term>
 443          <listitem>
 444            <para>Performs the corresponding <link linkend="whelp">query</link>,
 445             showing the result in the CIC browser. The command is removed
 446             from the script.
 447            </para>
 448          </listitem>
 449        </varlistentry>
 450      </variablelist>
 451    </para>
 452  </sect1>
 453  -->
 454  <sect1 id="command_qed">
 455    <title>qed</title>
 456    <para><userinput>qed</userinput></para>
 457    <para>
 458      <variablelist>
 459        <varlistentry>
 460          <term>Synopsis:</term>
 461          <listitem>
 462            <para><emphasis role="bold">qed</emphasis>
 463            </para>
 464          </listitem>
 465        </varlistentry>
 466        <varlistentry>
 467          <term>Action:</term>
 468          <listitem>
 469            <para>Saves and indexes the current interactive theorem or
 470             definition.
 471             In order to do this, the set of sequents still to be proved
 472             must be empty.</para>
 473          </listitem>
 474        </varlistentry>
 475      </variablelist>
 476    </para>
 477  </sect1>
 478  <sect1 id="command_qed_minus">
 479    <title>qed-</title>
 480    <para><userinput>qed-</userinput></para>
 481    <para>
 482      <variablelist>
 483        <varlistentry>
 484          <term>Synopsis:</term>
 485          <listitem>
 486            <para><emphasis role="bold">qed-</emphasis>
 487            </para>
 488          </listitem>
 489        </varlistentry>
 490        <varlistentry>
 491          <term>Action:</term>
 492          <listitem>
 493            <para>Saves the current interactive theorem or
 494             definition without indexing. Therefore automation will ignore
 495             it.
 496             In order to do this, the set of sequents still to be proved
 497             must be empty.</para>
 498          </listitem>
 499        </varlistentry>
 500      </variablelist>
 501    </para>
 502  </sect1>
 503  <sect1 id="command_unification_hint">
 504    <title>unification hint</title>
 505    <para>TODO</para>
 506    <!--
 507    <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
 508    <para>
 509      <variablelist>
 510        <varlistentry>
 511          <term>Synopsis:</term>
 512          <listitem>
 513                  <para>
 514                          <emphasis role="bold">coercion</emphasis>
 515                          (&uri; | &term; <emphasis role="bold">with</emphasis>)
 516                          [ &nat; [&nat;]]
 517                          [ <emphasis role="bold">nocomposites</emphasis> ]
 518                  </para>
 519          </listitem>
 520        </varlistentry>
 521        <varlistentry>
 522          <term>Action:</term>
 523          <listitem>
 524                  <para>Declares <command>u</command> as an implicit coercion.
 525                  If the type of <command>u</command> is
 526                  <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
 527                  <command>T(n - ariety)</command> while its source is
 528                  <command>T(n - ariety - saturation - 1)</command>.
 529             Every time a term <command>x</command>
 530             of type source is used with expected type target, Matita
 531             automatically replaces <command>x</command> with
 532             <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
 533             Note that the number of <command>?</command> added after
 534             <command>x</command> is saturation.
 535            <para>Implicit coercions are not displayed to the user:
 536             <command>(u ? … ? x)</command> is rendered simply
 537             as <command>x</command>.</para>
 538            <para>When a coercion <command>u</command> is declared
 539             from source <command>s</command> to target <command>t</command>
 540             and there is already a coercion <command>u'</command> of
 541             target <command>s</command> or source <command>t</command>,
 542             a composite implicit coercion is automatically computed
 543             by Matita unless <emphasis role="bold">nocomposites</emphasis>
 544             is specified.</para>
 545          </listitem>
 546        </varlistentry>
 547      </variablelist>
 548    </para>
 549    -->
 550  </sect1>
 551  <sect1 id="command_universe_constraints">
 552    <title>universe constraint</title>
 553    <para>TODO</para>
 554    <!--
 555    <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
 556    <para>
 557      <variablelist>
 558        <varlistentry>
 559          <term>Synopsis:</term>
 560          <listitem>
 561                  <para>
 562                          <emphasis role="bold">coercion</emphasis>
 563                          (&uri; | &term; <emphasis role="bold">with</emphasis>)
 564                          [ &nat; [&nat;]]
 565                          [ <emphasis role="bold">nocomposites</emphasis> ]
 566                  </para>
 567          </listitem>
 568        </varlistentry>
 569        <varlistentry>
 570          <term>Action:</term>
 571          <listitem>
 572                  <para>Declares <command>u</command> as an implicit coercion.
 573                  If the type of <command>u</command> is
 574                  <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
 575                  <command>T(n - ariety)</command> while its source is
 576                  <command>T(n - ariety - saturation - 1)</command>.
 577             Every time a term <command>x</command>
 578             of type source is used with expected type target, Matita
 579             automatically replaces <command>x</command> with
 580             <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
 581             Note that the number of <command>?</command> added after
 582             <command>x</command> is saturation.
 583            <para>Implicit coercions are not displayed to the user:
 584             <command>(u ? … ? x)</command> is rendered simply
 585             as <command>x</command>.</para>
 586            <para>When a coercion <command>u</command> is declared
 587             from source <command>s</command> to target <command>t</command>
 588             and there is already a coercion <command>u'</command> of
 589             target <command>s</command> or source <command>t</command>,
 590             a composite implicit coercion is automatically computed
 591             by Matita unless <emphasis role="bold">nocomposites</emphasis>
 592             is specified.</para>
 593          </listitem>
 594        </varlistentry>
 595      </variablelist>
 596    </para>
 597    -->
 598  </sect1>
 599
 600  <!--
 601  <sect1 id="command_inline">
 602    <title>inline</title>
 603    <para><userinput>inline &quot;s&quot; params</userinput></para>
 604    <para>
 605      <variablelist>
 606        <varlistentry>
 607          <term>Synopsis:</term>
 608          <listitem>
 609            <para>
 610              <emphasis role="bold">inline</emphasis> &qstring; &inlineparams;
 611            </para>
 612          </listitem>
 613        </varlistentry>
 614        <varlistentry>
 615          <term>Action:</term>
 616          <listitem>
 617            <para>Inlines a representation of the item <command>s</command>,
 618 which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
 619 URI) or the path of a *.ma source file is provided, all the contained objects
 620 are represented in a row.
 621 If the inlined object has a proof, this proof is represented in several ways
 622 depending on the provided parameters.</para>
 623          </listitem>
 624        </varlistentry>
 625      </variablelist>
 626    </para>
 627
 628     <sect2 id="inline-params">
 629     <title>inline-params</title>
 630     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 631       <title>inline-params</title>
 632       <tgroup cols="4">
 633       <tbody>
 634        <row>
 635         <entry id="grammar.inlineparams">&inlineparams;</entry>
 636         <entry>::=</entry>
 637         <entry>[&inlineparam; [&inlineparam;] … ]</entry>
 638        </row>
 639       </tbody>
 640      </tgroup>
 641     </table>
 642     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 643       <title>inline-param</title>
 644       <tgroup cols="4">
 645       <tbody>
 646
 647        <row>
 648         <entry id="grammar.inlineparam">&inlineparam;</entry>
 649         <entry>::=</entry>
 650         <entry><emphasis role="bold">axiom</emphasis></entry>
 651         <entry>Try to give an <link linkend="axiom">axiom</link> flavour
 652            (bodies are omitted even if present)
 653         </entry>
 654        </row>
 655
 656        <row>
 657         <entry/>
 658         <entry>|</entry>
 659         <entry><emphasis role="bold"> definition</emphasis></entry>
 660         <entry>Try give a <link linkend="definition">definition</link> flavour
 661         </entry>
 662        </row>
 663
 664        <row>
 665         <entry/>
 666         <entry>|</entry>
 667         <entry><emphasis role="bold">theorem</emphasis></entry>
 668         <entry>Try give a <link linkend="theorem">theorem</link> flavour
 669         </entry>
 670        </row>
 671
 672        <row>
 673         <entry/>
 674         <entry>|</entry>
 675         <entry><emphasis role="bold">lemma</emphasis></entry>
 676         <entry>Try give a <link linkend="lemma">lemma</link> flavour
 677         </entry>
 678        </row>
 679
 680        <row>
 681         <entry/>
 682         <entry>|</entry>
 683         <entry><emphasis role="bold">remark</emphasis></entry>
 684         <entry>Try give a <link linkend="remark">remark</link> flavour
 685         </entry>
 686        </row>
 687
 688        <row>
 689         <entry/>
 690         <entry>|</entry>
 691         <entry><emphasis role="bold">fact</emphasis></entry>
 692         <entry>Try give a <link linkend="fact">fact</link> flavour
 693         </entry>
 694        </row>
 695
 696        <row>
 697         <entry/>
 698         <entry>|</entry>
 699         <entry><emphasis role="bold">variant</emphasis></entry>
 700         <entry>Try give a <link linkend="variant">variant</link> flavour
 701                (implies <emphasis role="bold">plain</emphasis>)
 702         </entry>
 703        </row>
 704
 705        <row>
 706         <entry/>
 707         <entry>|</entry>
 708         <entry><emphasis role="bold">declarative</emphasis></entry>
 709         <entry>Represent proofs using
 710            <link linkend="sec_declarative_tactics">declarative tactics</link>
 711            (this is the dafault and can be omitted)
 712         </entry>
 713        </row>
 714
 715        <row>
 716         <entry/>
 717         <entry>|</entry>
 718         <entry><emphasis role="bold">procedural</emphasis></entry>
 719         <entry>Represent proofs using
 720            <link linkend="sec_tactics">procedural tactics</link>
 721         </entry>
 722        </row>
 723
 724        <row>
 725         <entry/>
 726         <entry>|</entry>
 727         <entry><emphasis role="bold">plain</emphasis></entry>
 728         <entry>Represent proofs using plain
 729            <link linkend="tbl_terms">proof terms</link>
 730         </entry>
 731        </row>
 732
 733        <row>
 734         <entry/>
 735         <entry>|</entry>
 736         <entry><emphasis role="bold">nodefaults</emphasis></entry>
 737         <entry>
 738          Do not use the tactics depending on the
 739          <link linkend="command_default">default</link> command
 740            (<link linkend="tac_rewrite">rewrite</link>
 741             in the <emphasis role="bold">procedural</emphasis> mode)
 742         </entry>
 743        </row>
 744
 745        <row valign="top">
 746         <entry/>
 747         <entry>|</entry>
 748         <entry><emphasis role="bold">level=&nat;</emphasis></entry>
 749         <entry>
 750          Set the level of the procedural proof representation
 751          (the default is the highest level)
 752          <itemizedlist>
 753           <listitem>
 754            Tactics used at level 1:
 755             <link linkend="tac_exact">exact</link>
 756           </listitem>
 757           <listitem>
 758            Additional tactics used at level 2:
 759             <link linkend="tac_letin">letin</link>,
 760             <link linkend="tac_cut">cut</link>,
 761             <link linkend="tac_change">change</link>,
 762             <link linkend="tac_intros">intros</link>,
 763             <link linkend="tac_apply">apply</link>,
 764             <link linkend="tac_elim">elim</link>,
 765             <link linkend="tac_cases">cases</link>,
 766             <link linkend="tac_rewrite">rewrite</link>
 767           </listitem>
 768          </itemizedlist>
 769         </entry>
 770        </row>
 771
 772        <row>
 773         <entry/>
 774         <entry>|</entry>
 775         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
 776         <entry>&TODO;</entry>
 777        </row>
 778
 779       </tbody>
 780      </tgroup>
 781     </table>
 782     </sect2>
 783  </sect1>
 784  -->
 785 </chapter>