helm/software/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 role="tactic.synopsis">
  13          <term>Synopsis:</term>
  14          <listitem>
  15            <para><emphasis role="bold">alias</emphasis>
  16             [<emphasis role="bold">id</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis> <emphasis role="bold">=</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis>
  17             | <emphasis role="bold">symbol</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis>
  18             | <emphasis role="bold">num</emphasis> [<emphasis role="bold">(instance</emphasis> &nat;<emphasis role="bold">)</emphasis>] <emphasis role="bold">=</emphasis> <emphasis role="bold">&quot;</emphasis>&string;<emphasis role="bold">&quot;</emphasis>
  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></userinput></para>
  58    <para>
  59      <variablelist>
  60        <varlistentry role="tactic.synopsis">
  61          <term>Synopsis:</term>
  62          <listitem>
  63            <para><emphasis role="bold">check</emphasis>
  64            </para>
  65          </listitem>
  66        </varlistentry>
  67        <varlistentry>
  68          <term>Action:</term>
  69          <listitem>
  70            <para>&TODO;</para>
  71          </listitem>
  72        </varlistentry>
  73      </variablelist>
  74    </para>
  75  </sect1>
  76  <sect1 id="command_coercion">
  77    <title>coercion</title>
  78    <para><userinput></userinput></para>
  79    <para>
  80      <variablelist>
  81        <varlistentry role="tactic.synopsis">
  82          <term>Synopsis:</term>
  83          <listitem>
  84            <para><emphasis role="bold">coercion</emphasis>
  85            </para>
  86          </listitem>
  87        </varlistentry>
  88        <varlistentry>
  89          <term>Action:</term>
  90          <listitem>
  91            <para>&TODO;</para>
  92          </listitem>
  93        </varlistentry>
  94      </variablelist>
  95    </para>
  96  </sect1>
  97  <sect1 id="command_default">
  98    <title>default</title>
  99    <para><userinput></userinput></para>
 100    <para>
 101      <variablelist>
 102        <varlistentry role="tactic.synopsis">
 103          <term>Synopsis:</term>
 104          <listitem>
 105            <para><emphasis role="bold">default</emphasis>
 106            </para>
 107          </listitem>
 108        </varlistentry>
 109        <varlistentry>
 110          <term>Action:</term>
 111          <listitem>
 112            <para>&TODO;</para>
 113          </listitem>
 114        </varlistentry>
 115      </variablelist>
 116    </para>
 117  </sect1>
 118  <sect1 id="command_hint">
 119    <title>hint</title>
 120    <para><userinput></userinput></para>
 121    <para>
 122      <variablelist>
 123        <varlistentry role="tactic.synopsis">
 124          <term>Synopsis:</term>
 125          <listitem>
 126            <para><emphasis role="bold">hint</emphasis>
 127            </para>
 128          </listitem>
 129        </varlistentry>
 130        <varlistentry>
 131          <term>Action:</term>
 132          <listitem>
 133            <para>&TODO;</para>
 134          </listitem>
 135        </varlistentry>
 136      </variablelist>
 137    </para>
 138  </sect1>
 139  <sect1 id="command_include">
 140    <title>include</title>
 141    <para><userinput></userinput></para>
 142    <para>
 143      <variablelist>
 144        <varlistentry role="tactic.synopsis">
 145          <term>Synopsis:</term>
 146          <listitem>
 147            <para><emphasis role="bold">include</emphasis>
 148            </para>
 149          </listitem>
 150        </varlistentry>
 151        <varlistentry>
 152          <term>Action:</term>
 153          <listitem>
 154            <para>&TODO;</para>
 155          </listitem>
 156        </varlistentry>
 157      </variablelist>
 158    </para>
 159  </sect1>
 160  <sect1 id="command_include_first">
 161    <title>include'</title>
 162    <para><userinput></userinput></para>
 163    <para>
 164      <variablelist>
 165        <varlistentry role="tactic.synopsis">
 166          <term>Synopsis:</term>
 167          <listitem>
 168            <para><emphasis role="bold">include'</emphasis>
 169            </para>
 170          </listitem>
 171        </varlistentry>
 172        <varlistentry>
 173          <term>Action:</term>
 174          <listitem>
 175            <para>&TODO;</para>
 176          </listitem>
 177        </varlistentry>
 178      </variablelist>
 179    </para>
 180  </sect1>
 181  <sect1 id="command_set">
 182    <title>set</title>
 183    <para><userinput></userinput></para>
 184    <para>
 185      <variablelist>
 186        <varlistentry role="tactic.synopsis">
 187          <term>Synopsis:</term>
 188          <listitem>
 189            <para><emphasis role="bold">set</emphasis>
 190            </para>
 191          </listitem>
 192        </varlistentry>
 193        <varlistentry>
 194          <term>Action:</term>
 195          <listitem>
 196            <para>&TODO;</para>
 197          </listitem>
 198        </varlistentry>
 199      </variablelist>
 200    </para>
 201  </sect1>
 202  <sect1 id="command_whelp">
 203    <title>whelp</title>
 204    <para><userinput></userinput></para>
 205    <para>
 206      <variablelist>
 207        <varlistentry role="tactic.synopsis">
 208          <term>Synopsis:</term>
 209          <listitem>
 210            <para><emphasis role="bold">whelp</emphasis>
 211            </para>
 212          </listitem>
 213        </varlistentry>
 214        <varlistentry>
 215          <term>Action:</term>
 216          <listitem>
 217            <para>&TODO;</para>
 218          </listitem>
 219        </varlistentry>
 220      </variablelist>
 221    </para>
 222  </sect1>
 223  <sect1 id="command_qed">
 224    <title>qed</title>
 225    <para><userinput></userinput></para>
 226    <para>
 227      <variablelist>
 228        <varlistentry role="tactic.synopsis">
 229          <term>Synopsis:</term>
 230          <listitem>
 231            <para><emphasis role="bold">qed</emphasis>
 232            </para>
 233          </listitem>
 234        </varlistentry>
 235        <varlistentry>
 236          <term>Action:</term>
 237          <listitem>
 238            <para>&TODO;</para>
 239          </listitem>
 240        </varlistentry>
 241      </variablelist>
 242    </para>
 243  </sect1>
 244 </chapter>
 245