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><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
   9       </row>
  10       <row>
  11         <entry/>
  12         <entry>|</entry>
  13         <entry><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
  14       </row>
  15       <row>
  16         <entry/>
  17         <entry>|</entry>
  18         <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>
  19       </row>
  20       <row>
  21         <entry/>
  22         <entry>|</entry>
  23         <entry>
  24           <link linkend="tac_assumption">
  25             <emphasis role="bold">assumption</emphasis>
  26           </link>
  27         </entry>
  28       </row>
  29       <row>
  30         <entry/>
  31         <entry>|</entry>
  32         <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
  33       </row>
  34       <row>
  35         <entry/>
  36         <entry>|</entry>
  37         <entry>
  38              <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
  39              <emphasis><link linkend="grammar.term">term</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
  40             </entry>
  41       </row>
  42       <row>
  43         <entry/>
  44         <entry>|</entry>
  45         <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>
  46       </row>
  47       <row>
  48         <entry/>
  49         <entry>|</entry>
  50         <entry>
  51              <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
  52              <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
  53             </entry>
  54       </row>
  55       <row>
  56         <entry/>
  57         <entry>|</entry>
  58         <entry><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></entry>
  59       </row>
  60       <row>
  61         <entry/>
  62         <entry>|</entry>
  63         <entry><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></entry>
  64       </row>
  65       <row>
  66         <entry/>
  67         <entry>|</entry>
  68         <entry>
  69           <link linkend="tac_contradiction">
  70             <emphasis role="bold">contradiction</emphasis>
  71           </link>
  72         </entry>
  73       </row>
  74       <row>
  75         <entry/>
  76         <entry>|</entry>
  77         <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
  78       </row>
  79       <row>
  80         <entry/>
  81         <entry>|</entry>
  82         <entry>
  83              <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
  84              [<emphasis role="bold">(</emphasis>
  85              <emphasis><link linkend="grammar.id">id</link></emphasis>…
  86              <emphasis role="bold">)</emphasis>]
  87              [<emphasis><link linkend="grammar.id">id</link></emphasis>]
  88              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
  89             </entry>
  90       </row>
  91       <row>
  92         <entry/>
  93         <entry>|</entry>
  94         <entry>
  95           <link linkend="tac_demodulate">
  96             <emphasis role="bold">demodulate</emphasis>
  97           </link>
  98         </entry>
  99       </row>
 100       <row>
 101         <entry/>
 102         <entry>|</entry>
 103         <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 104       </row>
 105       <row>
 106         <entry/>
 107         <entry>|</entry>
 108         <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
 109       </row>
 110       <row>
 111         <entry/>
 112         <entry>|</entry>
 113         <entry><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
 114       </row>
 115       <row>
 116         <entry/>
 117         <entry>|</entry>
 118         <entry><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 119       </row>
 120       <row>
 121         <entry/>
 122         <entry>|</entry>
 123         <entry>
 124           <link linkend="tac_exists">
 125             <emphasis role="bold">exists</emphasis>
 126           </link>
 127         </entry>
 128       </row>
 129       <row>
 130         <entry/>
 131         <entry>|</entry>
 132         <entry>
 133           <link linkend="tac_fail">
 134             <emphasis role="bold">fail</emphasis>
 135           </link>
 136         </entry>
 137       </row>
 138       <row>
 139         <entry/>
 140         <entry>|</entry>
 141         <entry><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 142       </row>
 143       <row>
 144         <entry/>
 145         <entry>|</entry>
 146         <entry>
 147           <link linkend="tac_fourier">
 148             <emphasis role="bold">fourier</emphasis>
 149           </link>
 150         </entry>
 151       </row>
 152       <row>
 153         <entry/>
 154         <entry>|</entry>
 155         <entry><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</entry>
 156       </row>
 157       <row>
 158         <entry/>
 159         <entry>|</entry>
 160         <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
 161       </row>
 162       <row>
 163         <entry/>
 164         <entry>|</entry>
 165         <entry>
 166           <link linkend="tac_id">
 167             <emphasis role="bold">id</emphasis>
 168           </link>
 169         </entry>
 170       </row>
 171       <row>
 172         <entry/>
 173         <entry>|</entry>
 174         <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
 175       </row>
 176       <row>
 177         <entry/>
 178         <entry>|</entry>
 179         <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
 180       </row>
 181       <row>
 182         <entry/>
 183         <entry>|</entry>
 184         <entry><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 185       </row>
 186       <row>
 187         <entry/>
 188         <entry>|</entry>
 189         <entry>
 190              <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
 191              [<emphasis role="bold">linear</emphasis>]
 192              [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
 193              <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 194              [<emphasis role="bold">to</emphasis>
 195               <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 196               [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
 197              ]
 198              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 199             </entry>
 200       </row>
 201       <row>
 202         <entry/>
 203         <entry>|</entry>
 204         <entry>
 205           <link linkend="tac_left">
 206             <emphasis role="bold">left</emphasis>
 207           </link>
 208         </entry>
 209       </row>
 210       <row>
 211         <entry/>
 212         <entry>|</entry>
 213         <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>
 214       </row>
 215       <row>
 216         <entry/>
 217         <entry>|</entry>
 218         <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 219       </row>
 220       <row>
 221         <entry/>
 222         <entry>|</entry>
 223         <entry><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 224       </row>
 225       <row>
 226         <entry/>
 227         <entry>|</entry>
 228         <entry>
 229           <link linkend="tac_reflexivity">
 230             <emphasis role="bold">reflexivity</emphasis>
 231           </link>
 232         </entry>
 233       </row>
 234       <row>
 235         <entry/>
 236         <entry>|</entry>
 237         <entry><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 238       </row>
 239       <row>
 240         <entry/>
 241         <entry>|</entry>
 242         <entry><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<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>
 243       </row>
 244       <row>
 245         <entry/>
 246         <entry>|</entry>
 247         <entry>
 248           <link linkend="tac_right">
 249             <emphasis role="bold">right</emphasis>
 250           </link>
 251         </entry>
 252       </row>
 253       <row>
 254         <entry/>
 255         <entry>|</entry>
 256         <entry>
 257           <link linkend="tac_ring">
 258             <emphasis role="bold">ring</emphasis>
 259           </link>
 260         </entry>
 261       </row>
 262       <row>
 263         <entry/>
 264         <entry>|</entry>
 265         <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 266       </row>
 267       <row>
 268         <entry/>
 269         <entry>|</entry>
 270         <entry>
 271           <link linkend="tac_split">
 272             <emphasis role="bold">split</emphasis>
 273           </link>
 274         </entry>
 275       </row>
 276       <row>
 277         <entry/>
 278         <entry>|</entry>
 279         <entry>
 280           <link linkend="tac_subst">
 281             <emphasis role="bold">subst</emphasis>
 282           </link>
 283         </entry>
 284       </row>
 285       <row>
 286         <entry/>
 287         <entry>|</entry>
 288         <entry>
 289           <link linkend="tac_symmetry">
 290             <emphasis role="bold">symmetry</emphasis>
 291           </link>
 292         </entry>
 293       </row>
 294       <row>
 295         <entry/>
 296         <entry>|</entry>
 297         <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 298       </row>
 299       <row>
 300         <entry/>
 301         <entry>|</entry>
 302         <entry><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 303       </row>
 304       <row>
 305         <entry/>
 306         <entry>|</entry>
 307         <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 308       </row>
 309     </tbody>
 310   </tgroup>
 311 </table>