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