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><userinput>unification hint n ≔ v1 : T1,… vi : Ti; h1 ≟ t1, …  hn ≟ tn ⊢ tl ≡ tr.</userinput></para>
 506    <para>
 507      <variablelist>
 508        <varlistentry>
 509          <term>Synopsis:</term>
 510          <listitem>
 511                  <para>
 512                          <emphasis role="bold">unification hint</emphasis>
 513                          &nat;
 514                          <emphasis role="bold">≔</emphasis>
 515                          [ &id; [ <emphasis role="bold">:</emphasis> &term; ] ,.. ]
 516                          <emphasis role="bold">;</emphasis>
 517                          [ &id; <emphasis role="bold">≟</emphasis> &term; ,.. ]
 518                          <emphasis role="bold">⊢</emphasis>
 519                          &term; <emphasis role="bold">≡</emphasis> &term;
 520                  </para>
 521          </listitem>
 522        </varlistentry>
 523        <varlistentry>
 524          <term>Action:</term>
 525          <listitem>
 526                  <para>Declares the hint at precedence <command>n</command></para>
 527                  <para>The file <command>hints_declaration.ma</command> must be
 528                          included to declare hints with that syntax.</para>
 529                  <para>Unification hints are described in the paper
 530                          &quot;Hints in unification&quot; by
 531                          Asperti, Ricciotti, Sacerdoti and Tassi.
 532                  </para>
 533          </listitem>
 534        </varlistentry>
 535      </variablelist>
 536    </para>
 537  </sect1>
 538  <sect1 id="command_universe_constraints">
 539    <title>universe constraint</title>
 540    <para>TODO</para>
 541    <!--
 542    <para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
 543    <para>
 544      <variablelist>
 545        <varlistentry>
 546          <term>Synopsis:</term>
 547          <listitem>
 548                  <para>
 549                          <emphasis role="bold">coercion</emphasis>
 550                          (&uri; | &term; <emphasis role="bold">with</emphasis>)
 551                          [ &nat; [&nat;]]
 552                          [ <emphasis role="bold">nocomposites</emphasis> ]
 553                  </para>
 554          </listitem>
 555        </varlistentry>
 556        <varlistentry>
 557          <term>Action:</term>
 558          <listitem>
 559                  <para>Declares <command>u</command> as an implicit coercion.
 560                  If the type of <command>u</command> is
 561                  <command>∀x1:T1. … ∀x(n-1):T(n-1).Tn</command> the coercion target is
 562                  <command>T(n - ariety)</command> while its source is
 563                  <command>T(n - ariety - saturation - 1)</command>.
 564             Every time a term <command>x</command>
 565             of type source is used with expected type target, Matita
 566             automatically replaces <command>x</command> with
 567             <command>(u ? … ? x ? … ?)</command> to avoid a typing error.</para>
 568             Note that the number of <command>?</command> added after
 569             <command>x</command> is saturation.
 570            <para>Implicit coercions are not displayed to the user:
 571             <command>(u ? … ? x)</command> is rendered simply
 572             as <command>x</command>.</para>
 573            <para>When a coercion <command>u</command> is declared
 574             from source <command>s</command> to target <command>t</command>
 575             and there is already a coercion <command>u'</command> of
 576             target <command>s</command> or source <command>t</command>,
 577             a composite implicit coercion is automatically computed
 578             by Matita unless <emphasis role="bold">nocomposites</emphasis>
 579             is specified.</para>
 580          </listitem>
 581        </varlistentry>
 582      </variablelist>
 583    </para>
 584    -->
 585  </sect1>
 586
 587  <!--
 588  <sect1 id="command_inline">
 589    <title>inline</title>
 590    <para><userinput>inline &quot;s&quot; params</userinput></para>
 591    <para>
 592      <variablelist>
 593        <varlistentry>
 594          <term>Synopsis:</term>
 595          <listitem>
 596            <para>
 597              <emphasis role="bold">inline</emphasis> &qstring; &inlineparams;
 598            </para>
 599          </listitem>
 600        </varlistentry>
 601        <varlistentry>
 602          <term>Action:</term>
 603          <listitem>
 604            <para>Inlines a representation of the item <command>s</command>,
 605 which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
 606 URI) or the path of a *.ma source file is provided, all the contained objects
 607 are represented in a row.
 608 If the inlined object has a proof, this proof is represented in several ways
 609 depending on the provided parameters.</para>
 610          </listitem>
 611        </varlistentry>
 612      </variablelist>
 613    </para>
 614
 615     <sect2 id="inline-params">
 616     <title>inline-params</title>
 617     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 618       <title>inline-params</title>
 619       <tgroup cols="4">
 620       <tbody>
 621        <row>
 622         <entry id="grammar.inlineparams">&inlineparams;</entry>
 623         <entry>::=</entry>
 624         <entry>[&inlineparam; [&inlineparam;] … ]</entry>
 625        </row>
 626       </tbody>
 627      </tgroup>
 628     </table>
 629     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 630       <title>inline-param</title>
 631       <tgroup cols="4">
 632       <tbody>
 633
 634        <row>
 635         <entry id="grammar.inlineparam">&inlineparam;</entry>
 636         <entry>::=</entry>
 637         <entry><emphasis role="bold">axiom</emphasis></entry>
 638         <entry>Try to give an <link linkend="axiom">axiom</link> flavour
 639            (bodies are omitted even if present)
 640         </entry>
 641        </row>
 642
 643        <row>
 644         <entry/>
 645         <entry>|</entry>
 646         <entry><emphasis role="bold"> definition</emphasis></entry>
 647         <entry>Try give a <link linkend="definition">definition</link> flavour
 648         </entry>
 649        </row>
 650
 651        <row>
 652         <entry/>
 653         <entry>|</entry>
 654         <entry><emphasis role="bold">theorem</emphasis></entry>
 655         <entry>Try give a <link linkend="theorem">theorem</link> flavour
 656         </entry>
 657        </row>
 658
 659        <row>
 660         <entry/>
 661         <entry>|</entry>
 662         <entry><emphasis role="bold">lemma</emphasis></entry>
 663         <entry>Try give a <link linkend="lemma">lemma</link> flavour
 664         </entry>
 665        </row>
 666
 667        <row>
 668         <entry/>
 669         <entry>|</entry>
 670         <entry><emphasis role="bold">remark</emphasis></entry>
 671         <entry>Try give a <link linkend="remark">remark</link> flavour
 672         </entry>
 673        </row>
 674
 675        <row>
 676         <entry/>
 677         <entry>|</entry>
 678         <entry><emphasis role="bold">fact</emphasis></entry>
 679         <entry>Try give a <link linkend="fact">fact</link> flavour
 680         </entry>
 681        </row>
 682
 683        <row>
 684         <entry/>
 685         <entry>|</entry>
 686         <entry><emphasis role="bold">variant</emphasis></entry>
 687         <entry>Try give a <link linkend="variant">variant</link> flavour
 688                (implies <emphasis role="bold">plain</emphasis>)
 689         </entry>
 690        </row>
 691
 692        <row>
 693         <entry/>
 694         <entry>|</entry>
 695         <entry><emphasis role="bold">declarative</emphasis></entry>
 696         <entry>Represent proofs using
 697            <link linkend="sec_declarative_tactics">declarative tactics</link>
 698            (this is the dafault and can be omitted)
 699         </entry>
 700        </row>
 701
 702        <row>
 703         <entry/>
 704         <entry>|</entry>
 705         <entry><emphasis role="bold">procedural</emphasis></entry>
 706         <entry>Represent proofs using
 707            <link linkend="sec_tactics">procedural tactics</link>
 708         </entry>
 709        </row>
 710
 711        <row>
 712         <entry/>
 713         <entry>|</entry>
 714         <entry><emphasis role="bold">plain</emphasis></entry>
 715         <entry>Represent proofs using plain
 716            <link linkend="tbl_terms">proof terms</link>
 717         </entry>
 718        </row>
 719
 720        <row>
 721         <entry/>
 722         <entry>|</entry>
 723         <entry><emphasis role="bold">nodefaults</emphasis></entry>
 724         <entry>
 725          Do not use the tactics depending on the
 726          <link linkend="command_default">default</link> command
 727            (<link linkend="tac_rewrite">rewrite</link>
 728             in the <emphasis role="bold">procedural</emphasis> mode)
 729         </entry>
 730        </row>
 731
 732        <row valign="top">
 733         <entry/>
 734         <entry>|</entry>
 735         <entry><emphasis role="bold">level=&nat;</emphasis></entry>
 736         <entry>
 737          Set the level of the procedural proof representation
 738          (the default is the highest level)
 739          <itemizedlist>
 740           <listitem>
 741            Tactics used at level 1:
 742             <link linkend="tac_exact">exact</link>
 743           </listitem>
 744           <listitem>
 745            Additional tactics used at level 2:
 746             <link linkend="tac_letin">letin</link>,
 747             <link linkend="tac_cut">cut</link>,
 748             <link linkend="tac_change">change</link>,
 749             <link linkend="tac_intros">intros</link>,
 750             <link linkend="tac_apply">apply</link>,
 751             <link linkend="tac_elim">elim</link>,
 752             <link linkend="tac_cases">cases</link>,
 753             <link linkend="tac_rewrite">rewrite</link>
 754           </listitem>
 755          </itemizedlist>
 756         </entry>
 757        </row>
 758
 759        <row>
 760         <entry/>
 761         <entry>|</entry>
 762         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
 763         <entry>&TODO;</entry>
 764        </row>
 765
 766       </tbody>
 767      </tgroup>
 768     </table>
 769     </sect2>
 770  </sect1>
 771  -->
 772 </chapter>