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