]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/basic_2/notation.ma
eb59a9d8f9bbc2bd55953ca26839913ad5c4db4f
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / notation.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
16
17 (* Grammar ******************************************************************)
18
19 notation "⓪"
20  non associative with precedence 90
21  for @{ 'Item0 }.
22
23 notation "hvbox( ⓪ { I } )"
24  non associative with precedence 90
25  for @{ 'Item0 $I }.
26
27 notation "⋆"
28  non associative with precedence 90
29  for @{ 'Star }.
30
31 notation "hvbox( ⋆ term 90 k )"
32  non associative with precedence 90
33  for @{ 'Star $k }.
34
35 notation "hvbox( # term 90 i )"
36  non associative with precedence 90
37  for @{ 'LRef $i }.
38
39 notation "hvbox( § term 90 p )"
40  non associative with precedence 90
41  for @{ 'GRef $p }.
42
43 notation "hvbox( ② term 55 T1 . break term 55 T )"
44  non associative with precedence 55
45  for @{ 'SnItem2 $T1 $T }.
46
47 notation "hvbox( ② { I } break term 55 T1 . break term 55 T )"
48  non associative with precedence 55
49  for @{ 'SnItem2 $I $T1 $T }.
50
51 notation "hvbox( ⓑ { a , I } break term 55 T1 . break term 55 T )"
52  non associative with precedence 55
53  for @{ 'SnBind2 $a $I $T1 $T }.
54
55 notation "hvbox( + ⓑ { I } break term 55 T1 . break term 55 T )"
56  non associative with precedence 55
57  for @{ 'SnBind2Pos $I $T1 $T }.
58
59 notation "hvbox( - ⓑ { I } break term 55 T1 . break term 55 T )"
60  non associative with precedence 55
61  for @{ 'SnBind2Neg $I $T1 $T }.
62
63 notation "hvbox( ⓕ { I } break term 55 T1 . break term 55 T )"
64  non associative with precedence 55
65  for @{ 'SnFlat2 $I $T1 $T }.
66
67 notation "hvbox( ⓓ { a } term 55 T1 . break term 55 T2 )"
68  non associative with precedence 55
69  for @{ 'SnAbbr $a $T1 $T2 }.
70
71 notation "hvbox( + ⓓ term 55 T1 . break term 55 T2 )"
72  non associative with precedence 55
73  for @{ 'SnAbbrPos $T1 $T2 }.
74
75 notation "hvbox( - ⓓ term 55 T1 . break term 55 T2 )"
76  non associative with precedence 55
77  for @{ 'SnAbbrNeg $T1 $T2 }.
78
79 notation "hvbox( ⓛ { a } term 55 T1 . break term 55 T2 )"
80  non associative with precedence 55
81  for @{ 'SnAbst $a $T1 $T2 }.
82
83 notation "hvbox( + ⓛ term 55 T1 . break term 55 T2 )"
84  non associative with precedence 55
85  for @{ 'SnAbstPos $T1 $T2 }.
86
87 notation "hvbox( - ⓛ term 55 T1 . break term 55 T2 )"
88  non associative with precedence 55
89  for @{ 'SnAbstNeg $T1 $T2 }.
90
91 notation "hvbox( ⓐ  term 55 T1 . break term 55 T2 )"
92  non associative with precedence 55
93  for @{ 'SnAppl $T1 $T2 }.
94
95 notation "hvbox( ⓝ  term 55 T1 . break term 55 T2 )"
96  non associative with precedence 55
97  for @{ 'SnCast $T1 $T2 }.
98
99 notation "hvbox( Ⓐ term 55 T1 . break term 55 T )"
100  non associative with precedence 55
101  for @{ 'SnApplV $T1 $T }.
102
103 notation > "hvbox( T . break ②{ I } break term 47 T1 )"
104  non associative with precedence 46
105  for @{ 'DxBind2 $T $I $T1 }.
106
107 notation "hvbox( T . break ⓑ { I } break term 48 T1 )"
108  non associative with precedence 47
109  for @{ 'DxBind2 $T $I $T1 }.
110
111 notation "hvbox( T1 . break ⓓ T2 )"
112  left associative with precedence 48
113  for @{ 'DxAbbr $T1 $T2 }.
114
115 notation "hvbox( T1 . break ⓛ T2 )"
116  left associative with precedence 49
117  for @{ 'DxAbst $T1 $T2 }.
118
119 notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )"
120  non associative with precedence 50
121  for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
122
123 notation "hvbox( # { x } )"
124  non associative with precedence 90
125  for @{ 'Weight $x }.
126
127 notation "hvbox( # { x , break y } )"
128  non associative with precedence 90
129  for @{ 'Weight $x $y }.
130
131 notation "hvbox( 𝐒  ⦃ T ⦄ )"
132    non associative with precedence 45
133    for @{ 'Simple $T }.
134
135 notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )"
136    non associative with precedence 45
137    for @{ 'Hom $L $T1 $T2 }.
138
139 notation "hvbox( T1 ≃ break term 46 T2 )"
140    non associative with precedence 45
141    for @{ 'Iso $T1 $T2 }.
142
143 (* Substitution *************************************************************)
144
145 notation "hvbox( ⇧ [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
146    non associative with precedence 45
147    for @{ 'RLift $d $e $T1 $T2 }.
148
149 notation "hvbox( T1 break ≼ [ d , break e ] break term 46 T2 )"
150    non associative with precedence 45
151    for @{ 'SubEq $T1 $d $e $T2 }.
152
153 notation "hvbox( ≽ [ d , break e ] break term 46 T2 )"
154    non associative with precedence 45
155    for @{ 'SubEqBottom $d $e $T2 }.
156
157 notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )"
158    non associative with precedence 45
159    for @{ 'RDrop $e $L1 $L2 }.
160
161 notation "hvbox( ⇩ [ d , break e ] break term 46 L1 ≡ break term 46 L2 )"
162    non associative with precedence 45
163    for @{ 'RDrop $d $e $L1 $L2 }.
164
165 notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ break ⦃ L2 , break T2 ⦄ )"
166    non associative with precedence 45
167    for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
168
169 notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )"
170    non associative with precedence 45
171    for @{ 'ICM $L $T $k }.
172
173 notation "hvbox( L ⊢ break term 46 T1 break ▶ [ d , break e ] break term 46 T2 )"
174    non associative with precedence 45
175    for @{ 'PSubst $L $T1 $d $e $T2 }.
176
177 (* Unfold *******************************************************************)
178
179 notation "hvbox( @ ⦃ T1 , break f ⦄ ≡ break term 46 T2 )"
180    non associative with precedence 45
181    for @{ 'RAt $T1 $f $T2 }.
182
183 notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )"
184    non associative with precedence 45
185    for @{ 'RMinus $T1 $T2 $T }.
186
187 notation "hvbox( ⇧ * [ e ] break term 46 T1 ≡ break term 46 T2 )"
188    non associative with precedence 45
189    for @{ 'RLiftStar $e $T1 $T2 }.
190
191 notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )"
192    non associative with precedence 45
193    for @{ 'RDropStar $e $L1 $L2 }.
194
195 notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ + break ⦃ L2 , break T2 ⦄ )"
196    non associative with precedence 45
197    for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }.
198
199 notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ * break ⦃ L2 , break T2 ⦄ )"
200    non associative with precedence 45
201    for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }.
202
203 notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )"
204    non associative with precedence 45
205    for @{ 'PSubstStar $T1 $d $e $T2 }.
206
207 notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ d , break e ] break term 46 T2 )"
208    non associative with precedence 45
209    for @{ 'PSubstStar $L $T1 $d $e $T2 }.
210
211 notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ d , break e ] break term 46 T2 )"
212    non associative with precedence 45
213    for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
214
215 notation "hvbox( T1 break ⊢ ▶ * [ d , break e ] break term 46 T2 )"
216    non associative with precedence 45
217    for @{ 'PSubstStarSn $T1 $d $e $T2 }.
218
219 notation "hvbox( T1 break ⊢ ▶ ▶ * [ d , break e ] break term 46 T2 )"
220    non associative with precedence 45
221    for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
222
223 notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
224    non associative with precedence 45
225    for @{ 'TSubst $T1 $d $e $T2 }.
226
227 notation "hvbox( L ⊢ break ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
228    non associative with precedence 45
229    for @{ 'TSubst $L $T1 $d $e $T2 }.
230
231 notation "hvbox( ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
232    non associative with precedence 45
233    for @{ 'TSubstAlt $T1 $d $e $T2 }.
234
235 notation "hvbox( L ⊢ break ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
236    non associative with precedence 45
237    for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
238
239 (* Static typing ************************************************************)
240
241 notation "hvbox( L ⊢ break term 46 T ⁝ break term 46 A )"
242    non associative with precedence 45
243    for @{ 'AtomicArity $L $T $A }.
244
245 notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )"
246    non associative with precedence 45
247    for @{ 'CrSubEqA $T1 $T2 }.
248
249 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T ÷ break term 46 A )"
250    non associative with precedence 45
251    for @{ 'BinaryArity $h $L $T $A }.
252
253 notation "hvbox( h ⊢ break term 46 L1 ÷ ⊑ break term 46 L2 )"
254    non associative with precedence 45
255    for @{ 'CrSubEqB $h $L1 $L2 }.
256
257 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break l ] break term 46 T2 )"
258    non associative with precedence 45
259    for @{ 'StaticType $h $g $l $L $T1 $T2 }.
260
261 notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )"
262    non associative with precedence 45
263    for @{ 'CrSubEqS $h $g $L1 $L2 }.
264
265 (* Unwind *******************************************************************)
266
267 notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )"
268    non associative with precedence 45
269    for @{ 'Unwind $L1 $T $L2 }.
270
271 (* Reducibility *************************************************************)
272
273 notation "hvbox( L ⊢ break 𝐑 ⦃ T ⦄ )"
274    non associative with precedence 45
275    for @{ 'Reducible $L $T }.
276
277 notation "hvbox( L ⊢ break 𝐈 ⦃ T ⦄ )"
278    non associative with precedence 45
279    for @{ 'NotReducible $L $T }.
280
281 notation "hvbox( L ⊢ break 𝐍 ⦃ T ⦄ )"
282    non associative with precedence 45
283    for @{ 'Normal $L $T }.
284
285 (* this might be removed *)
286 notation "hvbox( 𝐇𝐑 ⦃ T ⦄ )"
287    non associative with precedence 45
288    for @{ 'HdReducible $T }.
289
290 (* this might be removed *)
291 notation "hvbox( L ⊢ break 𝐇𝐑  ⦃ T ⦄ )"
292    non associative with precedence 45
293    for @{ 'HdReducible $L $T }.
294
295 (* this might be removed *)
296 notation "hvbox( 𝐇𝐈  ⦃ T ⦄ )"
297    non associative with precedence 45
298    for @{ 'NotHdReducible $T }.
299
300 (* this might be removed *)
301 notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ T ⦄ )"
302    non associative with precedence 45
303    for @{ 'NotHdReducible $L $T }.
304
305 (* this might be removed *)
306 notation "hvbox( 𝐇𝐍 ⦃ T ⦄ )"
307    non associative with precedence 45
308    for @{ 'HdNormal $T }.
309
310 (* this might be removed *)
311 notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ T ⦄ )"
312    non associative with precedence 45
313    for @{ 'HdNormal $L $T }.
314
315 notation "hvbox( T1 ➡ break term 46 T2 )"
316    non associative with precedence 45
317    for @{ 'PRed $T1 $T2 }.
318
319 notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )"
320    non associative with precedence 45
321    for @{ 'PRed $L $T1 $T2 }.
322
323 notation "hvbox( ⦃ L1 ⦄ ➡ break ⦃ L2 ⦄ )"
324    non associative with precedence 45
325    for @{ 'FocalizedPRed $L1 $L2 }.
326
327 notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
328    non associative with precedence 45
329    for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
330
331 notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
332    non associative with precedence 45
333    for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }.
334
335 notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )"
336    non associative with precedence 45
337    for @{ 'FocalizedPRedAlt $L1 $L2 }.
338
339 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ break [ g ] break term 46 T2 )"
340    non associative with precedence 45
341    for @{ 'XPRed $h $g $L $T1 $T2 }.
342
343 (* Computation **************************************************************)
344
345 notation "hvbox( T1 ➡ * break term 46 T2 )"
346    non associative with precedence 45
347    for @{ 'PRedStar $T1 $T2 }.
348
349 notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
350    non associative with precedence 45
351    for @{ 'PRedStar $L $T1 $T2 }.
352
353 notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
354    non associative with precedence 45
355    for @{ 'PRedStarAlt $T1 $T2 }.
356
357 notation "hvbox( ⦃ L1 ⦄ ➡ * break ⦃ L2 ⦄ )"
358    non associative with precedence 45
359    for @{ 'FocalizedPRedStar $L1 $L2 }.
360
361 notation "hvbox( ⦃ L1 , T1 ⦄ ➡ * break ⦃ L2 , T2 ⦄ )"
362    non associative with precedence 45
363    for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }.
364
365 notation "hvbox( ⦃ L1 ⦄ ➡ ➡ * break ⦃ L2 ⦄ )"
366    non associative with precedence 45
367    for @{ 'FocalizedPRedStarAlt $L1 $L2 }.
368
369 notation "hvbox( ⦃ L1 , T1 ⦄ ➡ ➡ * break ⦃ L2 , T2 ⦄ )"
370    non associative with precedence 45
371    for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
372
373 notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )"
374    non associative with precedence 45
375    for @{ 'PEval $L $T1 $T2 }.
376
377 notation "hvbox( ⬊ * term 46 T )"
378    non associative with precedence 45
379    for @{ 'SN $T }.
380
381 notation "hvbox( L ⊢ ⬊ * break term 46 T )"
382    non associative with precedence 45
383    for @{ 'SN $L $T }.
384
385 notation "hvbox( L ⊢ ⬊ ⬊ * break term 46 T )"
386    non associative with precedence 45
387    for @{ 'SNAlt $L $T }.
388
389 notation "hvbox( ⦃ L, break T ⦄ ϵ break [ R ] break 〚 A 〛 )"
390    non associative with precedence 45
391    for @{ 'InEInt $R $L $T $A }.
392
393 notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )"
394    non associative with precedence 45
395    for @{ 'CrSubEq $T1 $R $T2 }.
396
397 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ * break [ g ] break term 46 T2 )"
398    non associative with precedence 45
399    for @{ 'XPRedStar $h $g $L $T1 $T2 }.
400
401 notation "hvbox( ⦃ h , break L ⦄ ⊢ • ⬊ * break [ g ] break term 46 T2 )"
402    non associative with precedence 45
403    for @{ 'XSN $h $g $L $T }.
404
405 (* Conversion ***************************************************************)
406
407 notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
408    non associative with precedence 45
409    for @{ 'PConv $L $T1 $T2 }.
410
411 notation "hvbox( ⦃ L1 ⦄ ⬌ break ⦃ L2 ⦄ )"
412    non associative with precedence 45
413    for @{ 'FocalizedPConv $L1 $L2 }.
414
415 notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ break ⦃ L2 , break T2 ⦄ )"
416    non associative with precedence 45
417    for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }.
418
419 notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ break ⦃ L2 ⦄ )"
420    non associative with precedence 45
421    for @{ 'FocalizedPConvAlt $L1 $L2 }.
422
423 notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ break ⦃ L2 , break T2 ⦄ )"
424    non associative with precedence 45
425    for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
426
427 (* Equivalence **************************************************************)
428
429 notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )"
430    non associative with precedence 45
431    for @{ 'PConvStar $L $T1 $T2 }.
432
433 notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ g ] break term 46 L2 )"
434    non associative with precedence 45
435    for @{ 'CrSubEqSE $h $g $L1 $L2 }.
436
437 notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )"
438    non associative with precedence 45
439    for @{ 'FocalizedPConvStar $L1 $L2 }.
440
441 notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ * break ⦃ L2 , break T2 ⦄ )"
442    non associative with precedence 45
443    for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
444
445 notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ * break ⦃ L2 ⦄ )"
446    non associative with precedence 45
447    for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
448
449 notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ * break ⦃ L2 , break T2 ⦄ )"
450    non associative with precedence 45
451    for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
452
453 (* Dynamic typing ***********************************************************)
454
455 notation "hvbox( ⦃ h , break L ⦄ ⊩ break term 46 T : break [ g ] )"
456    non associative with precedence 45
457    for @{ 'NativeValid $h $g $L $T }.
458
459 notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ g ] break term 46 L2 )"
460    non associative with precedence 45
461    for @{ 'CrSubEqV $h $g $L1 $L2 }.
462
463 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
464    non associative with precedence 45
465    for @{ 'NativeType $h $L $T1 $T2 }.
466
467 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
468    non associative with precedence 45
469    for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
470
471 (* Higher order dynamic typing **********************************************)
472
473 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
474    non associative with precedence 45
475    for @{ 'NativeTypeStar $h $L $T1 $T2 }.