]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/Basic_2/notation.ma
- support for atomic arities and candidates of reducibility started
[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 "hvbox( ⋆ )"
20  non associative with precedence 90
21  for @{ 'Star }.
22
23 notation "hvbox( ⋆ term 90 k )"
24  non associative with precedence 90
25  for @{ 'Star $k }.
26
27 notation "hvbox( # term 90 i )"
28  non associative with precedence 90
29  for @{ 'LRef $i }.
30
31 notation "hvbox( § term 90 p )"
32  non associative with precedence 90
33  for @{ 'GRef $p }.
34
35 notation "hvbox( 𝕒 )"
36  non associative with precedence 90
37  for @{ 'SItem }.
38
39 notation "hvbox( 𝕒 { I } )"
40  non associative with precedence 90
41  for @{ 'SItem $I }.
42
43 notation "hvbox( 𝕔 term 90 T1 . break term 90 T )"
44  non associative with precedence 90
45  for @{ 'SItem $T1 $T }.
46
47 notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )"
48  non associative with precedence 90
49  for @{ 'SItem $I $T1 $T }.
50
51 notation "hvbox( 𝕓 { I } break term 90 T1 . break term 90 T )"
52  non associative with precedence 90
53  for @{ 'SBind $I $T1 $T }.
54
55 notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )"
56  non associative with precedence 90
57  for @{ 'SFlat $I $T1 $T }.
58
59 notation "hvbox( T . break 𝕓 { I } break term 90 T1 )"
60  non associative with precedence 89
61  for @{ 'DBind $T $I $T1 }.
62 (*
63 notation > "hvbox( T . break 𝕔 { I } break term 90 T1 )"
64  non associative with precedence 89
65  for @{ 'DBind $T $I $T1 }.
66 *) (**) (* this breaks all parsing *)
67 notation "hvbox( # [ x ] )"
68  non associative with precedence 90
69  for @{ 'Weight $x }.
70
71 notation "hvbox( # [ x , break y ] )"
72  non associative with precedence 90
73  for @{ 'Weight $x $y }.
74
75 notation "hvbox( 𝕊 [ T ] )"
76    non associative with precedence 45
77    for @{ 'Simple $T }.
78
79 notation "hvbox( T1 break [ d , break e ] ≼ break T2 )"
80    non associative with precedence 45
81    for @{ 'SubEq $T1 $d $e $T2 }.
82
83 (* Substitution *************************************************************)
84
85 notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )"
86    non associative with precedence 45
87    for @{ 'RLift $d $e $T1 $T2 }.
88
89 notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
90    non associative with precedence 45
91    for @{ 'RDrop $d $e $L1 $L2 }.
92
93 notation "hvbox( T1 break [ d , break e ] ≫ break T2 )"
94    non associative with precedence 45
95    for @{ 'PSubst $T1 $d $e $T2 }.
96
97 notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫ break T2 )"
98    non associative with precedence 45
99    for @{ 'PSubst $L $T1 $d $e $T2 }.
100
101 (* Unfold *******************************************************************)
102
103 notation "hvbox( T1 break [ d , break e ] ≫* break T2 )"
104    non associative with precedence 45
105    for @{ 'PSubstStar $T1 $d $e $T2 }.
106
107 notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫* break T2 )"
108    non associative with precedence 45
109    for @{ 'PSubstStar $L $T1 $d $e $T2 }.
110
111 notation "hvbox( T1 break [ d , break e ] ≡ break T2 )"
112    non associative with precedence 45
113    for @{ 'TSubst $T1 $d $e $T2 }.
114
115 notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
116    non associative with precedence 45
117    for @{ 'TSubst $L $T1 $d $e $T2 }.
118
119 (* Static Typing ************************************************************)
120
121 notation "hvbox( L ⊢ break term 90 T ÷ break A )"
122    non associative with precedence 45
123    for @{ 'AtomicArity $L $T $A }.
124
125 (* Reducibility *************************************************************)
126
127 notation "hvbox( ℝ [ T ] )"
128    non associative with precedence 45
129    for @{ 'Reducible $T }.
130
131 notation "hvbox( L ⊢ ℝ [ T ] )"
132    non associative with precedence 45
133    for @{ 'Reducible $L $T }.
134
135 notation "hvbox( 𝕀 [ T ] )"
136    non associative with precedence 45
137    for @{ 'NotReducible $T }.
138
139 notation "hvbox( L ⊢ 𝕀 [ T ] )"
140    non associative with precedence 45
141    for @{ 'NotReducible $L $T }.
142
143 notation "hvbox( ℕ [ T ] )"
144    non associative with precedence 45
145    for @{ 'Normal $T }.
146
147 notation "hvbox( L ⊢ ℕ [ T ] )"
148    non associative with precedence 45
149    for @{ 'Normal $L $T }.
150
151 notation "hvbox( 𝕎ℍℝ [ T ] )"
152    non associative with precedence 45
153    for @{ 'WHdReducible $T }.
154
155 notation "hvbox( L ⊢ 𝕎ℍℝ [ T ] )"
156    non associative with precedence 45
157    for @{ 'WHdReducible $L $T }.
158
159 notation "hvbox( 𝕎ℍ𝕀 [ T ] )"
160    non associative with precedence 45
161    for @{ 'NotWHdReducible $T }.
162
163 notation "hvbox( L ⊢ 𝕎ℍ𝕀 [ T ] )"
164    non associative with precedence 45
165    for @{ 'NotWHdReducible $L $T }.
166
167 notation "hvbox( 𝕎ℍℕ [ T ] )"
168    non associative with precedence 45
169    for @{ 'WHdNormal $T }.
170
171 notation "hvbox( L ⊢ 𝕎ℍℕ [ T ] )"
172    non associative with precedence 45
173    for @{ 'WHdNormal $L $T }.
174
175 notation "hvbox( T1 ⇒ break T2 )"
176    non associative with precedence 45
177    for @{ 'PRed $T1 $T2 }.
178
179 notation "hvbox( L ⊢ break term 90 T1 ⇒ break T2 )"
180    non associative with precedence 45
181    for @{ 'PRed $L $T1 $T2 }.
182
183 notation "hvbox( L1 ⊢ ⇒ break L2 )"
184    non associative with precedence 45
185    for @{ 'CPRed $L1 $L2 }.
186
187 (* Computation **************************************************************)
188
189 notation "hvbox( T1 ⇒* break T2 )"
190    non associative with precedence 45
191    for @{ 'PRedStar $T1 $T2 }.
192
193 notation "hvbox( L ⊢ break term 90 T1 ⇒* break T2 )"
194    non associative with precedence 45
195    for @{ 'PRedStar $L $T1 $T2 }.
196
197 notation "hvbox( L1 ⊢ ⇒* break L2 )"
198    non associative with precedence 45
199    for @{ 'CPRedStar $L1 $L2 }.
200
201 notation "hvbox( ⇓ T  )"
202    non associative with precedence 45
203    for @{ 'SN $T }.
204
205 notation "hvbox( L ⊢ ⇓ T )"
206    non associative with precedence 45
207    for @{ 'SN $L $T }.
208
209 notation "hvbox( { L, break T } ϵ break 〚 A 〛 )"
210    non associative with precedence 45
211    for @{ 'InEInt $L $T $A }.
212
213 notation "hvbox( R ⊢ break { L, break T } ϵ break 〚 A 〛 )"
214    non associative with precedence 45
215    for @{ 'InEInt $R $L $T $A }.
216
217 notation "hvbox( T1 ⊑ break T2 )"
218    non associative with precedence 45
219    for @{ 'CrSubEq $T1 $T2 }.
220
221 notation "hvbox( T1 break [ R ] ⊑ break T2 )"
222    non associative with precedence 45
223    for @{ 'CrSubEq $T1 $R $T2 }.