helm/www/matita/docs/manual-0.5.9/command_inline.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>inline</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="sec_commands.html" title="Chapter 9. Other commands" /><link rel="prev" href="command_qed.html" title="qed" /><link rel="next" href="sec_license.html" title="Chapter 10. License" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">inline</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="command_qed.html">Prev</a> </td><th width="60%" align="center">Chapter 9. Other commands</th><td width="20%" align="right"> <a accesskey="n" href="sec_license.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="command_inline"></a>inline</h2></div></div></div><p><strong class="userinput"><code>inline "s" params</code></strong></p><p>
   3      </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p>
   4              <span class="bold"><strong>inline</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.qstring">qstring</a></em></span> <span class="emphasis"><em><a class="link" href="command_inline.html#grammar.inlineparams">inline_params</a></em></span>
   5            </p></dd><dt><span class="term">Action:</span></dt><dd><p>Inlines a representation of the item <span class="command"><strong>s</strong></span>,
   6 which can be the URI of a HELM object. If an entire HELM directory (i.e. a base
   7 URI) or the path of a *.ma source file is provided, all the contained objects
   8 are represented in a row.
   9 If the inlined object has a proof, this proof is represented in several ways
  10 depending on the provided parameters.</p></dd></dl></div><p>
  11    </p><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="inline-params"></a>inline-params</h3></div></div></div><div class="table"><a id="idp73947536"></a><p class="title"><strong>Table 9.2. inline-params</strong></p><div class="table-contents"><table summary="inline-params" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.inlineparams"></a><span class="emphasis"><em><a class="link" href="command_inline.html#grammar.inlineparams">inline_params</a></em></span></td><td style="">::=</td><td style="">[<span class="emphasis"><em><a class="link" href="command_inline.html#grammar.inlineparam">inline_param</a></em></span> [<span class="emphasis"><em><a class="link" href="command_inline.html#grammar.inlineparam">inline_param</a></em></span>] … ]</td><td class="auto-generated" style=""> </td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idp73955728"></a><p class="title"><strong>Table 9.3. inline-param</strong></p><div class="table-contents"><table summary="inline-param" style="border-collapse: collapse;border-top: 0.5pt solid ; border-bottom: 0.5pt solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.inlineparam"></a><span class="emphasis"><em><a class="link" href="command_inline.html#grammar.inlineparam">inline_param</a></em></span></td><td style="">::=</td><td style=""><span class="bold"><strong>axiom</strong></span></td><td style="">Try to give an <a class="link" href="axiom_definition_declaration.html#axiom" title="axiom id: term">axiom</a> flavour
  12            (bodies are omitted even if present)
  13         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>definition</strong></span></td><td style="">Try give a <a class="link" href="axiom_definition_declaration.html#definition" title="definition id[: term] [≝ term]">definition</a> flavour
  14         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>theorem</strong></span></td><td style="">Try give a <a class="link" href="proofs.html#theorem" title="theorem id[: term] [≝ term]">theorem</a> flavour
  15         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>lemma</strong></span></td><td style="">Try give a <a class="link" href="proofs.html#lemma" title="lemma id[: term] [≝ term]">lemma</a> flavour
  16         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>remark</strong></span></td><td style="">Try give a <a class="link" href="proofs.html#remark" title="remark id[: term] [≝ term]">remark</a> flavour
  17         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>fact</strong></span></td><td style="">Try give a <a class="link" href="proofs.html#fact" title="fact id[: term] [≝ term]">fact</a> flavour
  18         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>variant</strong></span></td><td style="">Try give a <a class="link" href="proofs.html#variant" title="variant id: term ≝ term">variant</a> flavour
  19                (implies <span class="bold"><strong>plain</strong></span>)
  20         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>declarative</strong></span></td><td style="">Represent proofs using
  21            <a class="link" href="sec_declarative_tactics.html" title="Chapter 8. Declarative Tactics">declarative tactics</a>
  22            (this is the dafault and can be omitted)
  23         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>procedural</strong></span></td><td style="">Represent proofs using
  24            <a class="link" href="sec_tactics.html" title="Chapter 7. Tactics">procedural tactics</a>
  25         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>plain</strong></span></td><td style="">Represent proofs using plain
  26            <a class="link" href="sec_terms.html#tbl_terms" title="Table 4.9. Terms">proof terms</a>
  27         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>nodefaults</strong></span></td><td style="">
  28          Do not use the tactics depending on the
  29          <a class="link" href="command_default.html" title="default">default</a> command
  30            (<a class="link" href="tac_rewrite.html" title="rewrite">rewrite</a>
  31             in the <span class="bold"><strong>procedural</strong></span> mode)
  32         </td></tr><tr valign="top"><td style="" valign="top"> </td><td style="" valign="top">|</td><td style="" valign="top"><span class="bold"><strong>level=<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></strong></span></td><td style="" valign="top">
  33          Set the level of the procedural proof representation
  34          (the default is the highest level)
  35          <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; "><li class="listitem">
  36            Tactics used at level 1:
  37             <a class="link" href="tac_exact.html" title="exact">exact</a></li><li class="listitem">
  38            Additional tactics used at level 2:
  39             <a class="link" href="tac_letin.html" title="letin">letin</a>,
  40             <a class="link" href="tac_cut.html" title="cut">cut</a>,
  41             <a class="link" href="tac_change.html" title="change">change</a>,
  42             <a class="link" href="tac_intros.html" title="intros">intros</a>,
  43             <a class="link" href="tac_apply.html" title="apply">apply</a>,
  44             <a class="link" href="tac_elim.html" title="elim">elim</a>,
  45             <a class="link" href="tac_cases.html" title="cases">cases</a>,
  46             <a class="link" href="tac_rewrite.html" title="rewrite">rewrite</a></li></ul></div>
  47         </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>depth=<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span></strong></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr></tbody></table></div></div><br class="table-break" /></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="command_qed.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_commands.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_license.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">qed </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 10. License</td></tr></table></div></body></html>