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