matita/matita/help/C/tactics_quickref.xml

   1 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
   2   <title>tactics</title>
   3   <tgroup cols="3">
   4     <tbody>
   5       <row>
   6         <entry id="grammar.tactic">&tactic;</entry>
   7         <entry>::=</entry>
   8         <entry><emphasis role="bold">@</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
   9       </row>
  10       <row>
  11         <entry/>
  12         <entry>|</entry>
  13         <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
  14       </row>
  15       <row>
  16         <entry/>
  17         <entry>|</entry>
  18         <entry>
  19           <link linkend="tac_assumption">
  20             <emphasis role="bold">assumption</emphasis>
  21           </link>
  22         </entry>
  23       </row>
  24       <row>
  25         <entry/>
  26         <entry>|</entry>
  27         <entry><emphasis role="bold">/</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">/</emphasis>. </entry>
  28       </row>
  29       <row>
  30         <entry/>
  31         <entry>|</entry>
  32         <entry>
  33              <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
  34              <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
  35             </entry>
  36       </row>
  37       <row>
  38         <entry/>
  39         <entry>|</entry>
  40         <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
  41       </row>
  42       <row>
  43         <entry/>
  44         <entry>|</entry>
  45         <entry>
  46              <emphasis role="bold">-</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
  47             </entry>
  48       </row>
  49       <row>
  50         <entry/>
  51         <entry>|</entry>
  52         <entry><emphasis role="bold">%</emphasis> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bol">{</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…<emphasis role="bol">}</emphasis>]</entry>
  53       </row>
  54       <row>
  55         <entry/>
  56         <entry>|</entry>
  57         <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
  58       </row>
  59       <row>
  60         <entry/>
  61         <entry>|</entry>
  62         <entry>
  63              <emphasis role="bold">*</emphasis>
  64              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
  65             </entry>
  66       </row>
  67       <row>
  68         <entry/>
  69         <entry>|</entry>
  70         <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link>
  71              [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>]</entry>
  72       </row>
  73       <row>
  74         <entry/>
  75         <entry>|</entry>
  76         <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
  77       </row>
  78       <row>
  79         <entry/>
  80         <entry>|</entry>
  81         <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
  82       </row>
  83       <row>
  84         <entry/>
  85         <entry>|</entry>
  86         <entry>
  87           <emphasis role="bold">#</emphasis>
  88           <emphasis>
  89             <link linkend="grammar.id">id</link>
  90           </emphasis>
  91         </entry>
  92       </row>
  93       <row>
  94         <entry/>
  95         <entry>|</entry>
  96         <entry>
  97           <emphasis role="bold">#_</emphasis>
  98         </entry>
  99       </row>
 100       <row>
 101         <entry/>
 102         <entry>|</entry>
 103         <entry><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 104       </row>
 105       <row>
 106         <entry/>
 107         <entry>|</entry>
 108         <entry>
 109              <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
 110              <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 111             </entry>
 112       </row>
 113       <row>
 114         <entry/>
 115         <entry>|</entry>
 116         <entry><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 117       </row>
 118       <row>
 119         <entry/>
 120         <entry>|</entry>
 121         <entry>
 122           <emphasis role="bold">##</emphasis>
 123         </entry>
 124       </row>
 125       <row>
 126         <entry/>
 127         <entry>|</entry>
 128         <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
 129              [<emphasis role="bold">nodelta</emphasis>]</entry>
 130       </row>
 131       <row>
 132         <entry/>
 133         <entry>|</entry>
 134         <entry>[<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 135       </row>
 136       <row>
 137         <entry/>
 138         <entry>|</entry>
 139         <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
 140       </row>
 141     </tbody>
 142   </tgroup>
 143 </table>