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