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">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
  85             </entry>
  86       </row>
  87       <row>
  88         <entry/>
  89         <entry>|</entry>
  90         <entry>
  91           <link linkend="tac_demodulate">
  92             <emphasis role="bold">demodulate</emphasis>
  93           </link>
  94         </entry>
  95       </row>
  96       <row>
  97         <entry/>
  98         <entry>|</entry>
  99         <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 100       </row>
 101       <row>
 102         <entry/>
 103         <entry>|</entry>
 104         <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>
 105       </row>
 106       <row>
 107         <entry/>
 108         <entry>|</entry>
 109         <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>
 110       </row>
 111       <row>
 112         <entry/>
 113         <entry>|</entry>
 114         <entry><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 115       </row>
 116       <row>
 117         <entry/>
 118         <entry>|</entry>
 119         <entry>
 120           <link linkend="tac_exists">
 121             <emphasis role="bold">exists</emphasis>
 122           </link>
 123         </entry>
 124       </row>
 125       <row>
 126         <entry/>
 127         <entry>|</entry>
 128         <entry>
 129           <link linkend="tac_fail">
 130             <emphasis role="bold">fail</emphasis>
 131           </link>
 132         </entry>
 133       </row>
 134       <row>
 135         <entry/>
 136         <entry>|</entry>
 137         <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>
 138       </row>
 139       <row>
 140         <entry/>
 141         <entry>|</entry>
 142         <entry>
 143           <link linkend="tac_fourier">
 144             <emphasis role="bold">fourier</emphasis>
 145           </link>
 146         </entry>
 147       </row>
 148       <row>
 149         <entry/>
 150         <entry>|</entry>
 151         <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>
 152       </row>
 153       <row>
 154         <entry/>
 155         <entry>|</entry>
 156         <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>
 157       </row>
 158       <row>
 159         <entry/>
 160         <entry>|</entry>
 161         <entry>
 162           <link linkend="tac_id">
 163             <emphasis role="bold">id</emphasis>
 164           </link>
 165         </entry>
 166       </row>
 167       <row>
 168         <entry/>
 169         <entry>|</entry>
 170         <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
 171       </row>
 172       <row>
 173         <entry/>
 174         <entry>|</entry>
 175         <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
 176       </row>
 177       <row>
 178         <entry/>
 179         <entry>|</entry>
 180         <entry><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 181       </row>
 182       <row>
 183         <entry/>
 184         <entry>|</entry>
 185         <entry>
 186              <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
 187              [<emphasis role="bold">linear</emphasis>]
 188              [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
 189              <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 190              [<emphasis role="bold">to</emphasis>
 191               <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
 192               [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
 193              ]
 194              [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 195             </entry>
 196       </row>
 197       <row>
 198         <entry/>
 199         <entry>|</entry>
 200         <entry>
 201           <link linkend="tac_left">
 202             <emphasis role="bold">left</emphasis>
 203           </link>
 204         </entry>
 205       </row>
 206       <row>
 207         <entry/>
 208         <entry>|</entry>
 209         <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>
 210       </row>
 211       <row>
 212         <entry/>
 213         <entry>|</entry>
 214         <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 215       </row>
 216       <row>
 217         <entry/>
 218         <entry>|</entry>
 219         <entry><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 220       </row>
 221       <row>
 222         <entry/>
 223         <entry>|</entry>
 224         <entry>
 225           <link linkend="tac_reflexivity">
 226             <emphasis role="bold">reflexivity</emphasis>
 227           </link>
 228         </entry>
 229       </row>
 230       <row>
 231         <entry/>
 232         <entry>|</entry>
 233         <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>
 234       </row>
 235       <row>
 236         <entry/>
 237         <entry>|</entry>
 238         <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>
 239       </row>
 240       <row>
 241         <entry/>
 242         <entry>|</entry>
 243         <entry>
 244           <link linkend="tac_right">
 245             <emphasis role="bold">right</emphasis>
 246           </link>
 247         </entry>
 248       </row>
 249       <row>
 250         <entry/>
 251         <entry>|</entry>
 252         <entry>
 253           <link linkend="tac_ring">
 254             <emphasis role="bold">ring</emphasis>
 255           </link>
 256         </entry>
 257       </row>
 258       <row>
 259         <entry/>
 260         <entry>|</entry>
 261         <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 262       </row>
 263       <row>
 264         <entry/>
 265         <entry>|</entry>
 266         <entry>
 267           <link linkend="tac_split">
 268             <emphasis role="bold">split</emphasis>
 269           </link>
 270         </entry>
 271       </row>
 272       <row>
 273         <entry/>
 274         <entry>|</entry>
 275         <entry>
 276           <link linkend="tac_subst">
 277             <emphasis role="bold">subst</emphasis>
 278           </link>
 279         </entry>
 280       </row>
 281       <row>
 282         <entry/>
 283         <entry>|</entry>
 284         <entry>
 285           <link linkend="tac_symmetry">
 286             <emphasis role="bold">symmetry</emphasis>
 287           </link>
 288         </entry>
 289       </row>
 290       <row>
 291         <entry/>
 292         <entry>|</entry>
 293         <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
 294       </row>
 295       <row>
 296         <entry/>
 297         <entry>|</entry>
 298         <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>
 299       </row>
 300       <row>
 301         <entry/>
 302         <entry>|</entry>
 303         <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
 304       </row>
 305     </tbody>
 306   </tgroup>
 307 </table>