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>check t</userinput></para>
  58    <para>
  59      <variablelist>
  60        <varlistentry role="tactic.synopsis">
  61          <term>Synopsis:</term>
  62          <listitem>
  63            <para><emphasis role="bold">check &term;</emphasis>
  64            </para>
  65          </listitem>
  66        </varlistentry>
  67        <varlistentry>
  68          <term>Action:</term>
  69          <listitem>
  70            <para>Opens a CIC browser window that shows <command>t</command>
  71             together with its type. The command is immediately removed from
  72             the script.</para>
  73          </listitem>
  74        </varlistentry>
  75      </variablelist>
  76    </para>
  77  </sect1>
  78  <sect1 id="command_coercion">
  79    <title>coercion</title>
  80    <para><userinput>coercion u</userinput></para>
  81    <para>
  82      <variablelist>
  83        <varlistentry role="tactic.synopsis">
  84          <term>Synopsis:</term>
  85          <listitem>
  86            <para><emphasis role="bold">coercion &uri;</emphasis>
  87            </para>
  88          </listitem>
  89        </varlistentry>
  90        <varlistentry>
  91          <term>Action:</term>
  92          <listitem>
  93            <para>Declares <command>u</command> as an implicit coercion
  94             from the type of its last argument (source)
  95             to its codomain (target). Every time a term <command>x</command>
  96             of type source is used with expected type target, Matita
  97             automatically replaces <command>x</command> with
  98             <command>(u ? … ? x)</command> to avoid a typing error.</para>
  99            <para>Implicit coercions are not displayed to the user:
 100             <command>(u ? … ? x)</command> is rendered simply
 101             as <command>x</command>.</para>
 102            <para>When a coercion <command>u</command> is declared
 103             from source <command>s</command> to target <command>t</command>
 104             and there is already a coercion <command>u'</command> of
 105             target <command>s</command> or source <command>t</command>,
 106             a composite implicit coercion is automatically computed
 107             by Matita.</para>
 108          </listitem>
 109        </varlistentry>
 110      </variablelist>
 111    </para>
 112  </sect1>
 113  <sect1 id="command_default">
 114    <title>default</title>
 115    <para><userinput></userinput></para>
 116    <para>
 117      <variablelist>
 118        <varlistentry role="tactic.synopsis">
 119          <term>Synopsis:</term>
 120          <listitem>
 121            <para><emphasis role="bold">default</emphasis>
 122            </para>
 123          </listitem>
 124        </varlistentry>
 125        <varlistentry>
 126          <term>Action:</term>
 127          <listitem>
 128            <para>&TODO;</para>
 129          </listitem>
 130        </varlistentry>
 131      </variablelist>
 132    </para>
 133  </sect1>
 134  <sect1 id="command_hint">
 135    <title>hint</title>
 136    <para><userinput>hint</userinput></para>
 137    <para>
 138      <variablelist>
 139        <varlistentry role="tactic.synopsis">
 140          <term>Synopsis:</term>
 141          <listitem>
 142            <para><emphasis role="bold">hint</emphasis>
 143            </para>
 144          </listitem>
 145        </varlistentry>
 146        <varlistentry>
 147          <term>Action:</term>
 148          <listitem>
 149            <para>Displays a list of theorems that can be successfully
 150             applied to the current selected sequent. The command is
 151             removed from the script, but the window that displays the
 152             theorems allow to add to the script the application of the
 153             selected theorem.
 154            </para>
 155          </listitem>
 156        </varlistentry>
 157      </variablelist>
 158    </para>
 159  </sect1>
 160  <sect1 id="command_include">
 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_include_first">
 182    <title>include'</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">include'</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_set">
 203    <title>set</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">set</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_whelp">
 224    <title>whelp</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">whelp</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  <sect1 id="command_qed">
 245    <title>qed</title>
 246    <para><userinput></userinput></para>
 247    <para>
 248      <variablelist>
 249        <varlistentry role="tactic.synopsis">
 250          <term>Synopsis:</term>
 251          <listitem>
 252            <para><emphasis role="bold">qed</emphasis>
 253            </para>
 254          </listitem>
 255        </varlistentry>
 256        <varlistentry>
 257          <term>Action:</term>
 258          <listitem>
 259            <para>Saves and indexes the current interactive theorem or
 260             definition.
 261             In order to do this, the set of sequents still to be proved
 262             must be empty.</para>
 263          </listitem>
 264        </varlistentry>
 265      </variablelist>
 266    </para>
 267  </sect1>
 268 </chapter>
 269