matita/matita/lib/hott/notations.ma

   1 notation "1" with precedence 90 for @{'idpath}.
   2
   3 notation < "hvbox(l1 break # _(term 90 F) (term 47 l2))"
   4   non associative with precedence 47
   5   for @{'transport $F $l1 $l2 }.
   6
   7 notation > "hvbox(l1 break # l2)"
   8   right associative with precedence 47
   9   for @{'transport ? $l1 $l2 }.
  10
  11 notation "hvbox(l1 break @ l2)"
  12   right associative with precedence 49
  13   for @{'append $l1 $l2 }.
  14
  15 (* exists *******************************************************************)
  16
  17 notation "hvbox(∃ _ break . p)"
  18  with precedence 20
  19 for @{'exists $p }.
  20
  21 notation < "hvbox(\exists ident i : ty break . p)"
  22  right associative with precedence 20
  23 for @{'exists (\lambda ${ident i} : $ty. $p) }.
  24
  25 notation < "hvbox(\exists ident i break . p)"
  26   with precedence 20
  27 for @{'exists (\lambda ${ident i}. $p) }.
  28
  29 notation "hvbox(〈term 19 a, break term 19 b〉)"
  30 with precedence 90 for @{ 'mk_exists $a $b }.
  31
  32 (*
  33 notation < "hvbox(\exists ident i opt (: ty) break . p)"
  34   right associative with precedence 20
  35 for @{ 'exists ${default
  36   @{\lambda ${ident i} : $ty. $p}
  37   @{\lambda ${ident i} . $p}}}.
  38 *)
  39
  40 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
  41   with precedence 20
  42   for ${ default
  43           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
  44           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
  45        }.
  46
  47 (*
  48 notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
  49  non associative with precedence 20
  50  for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
  51
  52 notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
  53  non associative with precedence 20
  54  for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
  55
  56 (* sigma ********************************************************************)
  57
  58 notation < "hvbox(\Sigma ident i : ty break . p)"
  59  left associative with precedence 20
  60 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
  61
  62 notation < "hvbox(\Sigma ident i break . p)"
  63  with precedence 20
  64 for @{'sigma (\lambda ${ident i}. $p) }.
  65
  66 (*
  67 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
  68   right associative with precedence 20
  69 for @{ 'sigma ${default
  70   @{\lambda ${ident i} : $ty. $p}
  71   @{\lambda ${ident i} . $p}}}.
  72 *)
  73
  74 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
  75   with precedence 20
  76   for ${ default
  77           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
  78           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
  79        }.
  80
  81 notation "hvbox(« term 19 a, break term 19 b»)"
  82 with precedence 90 for @{ 'dp $a $b }.
  83
  84 (* dependent pairs (i.e. Sigma with predicate in Type[0])  ********************)
  85
  86 notation < "hvbox(𝚺 ident i : ty break . p)"
  87  left associative with precedence 20
  88 for @{'dpair (\lambda ${ident i} : $ty. $p) }.
  89
  90 notation < "hvbox(𝚺 ident i break . p)"
  91  with precedence 20
  92 for @{'dpair (\lambda ${ident i}. $p) }.
  93
  94 (*
  95 notation < "hvbox(𝚺 ident i opt (: ty) break . p)"
  96   right associative with precedence 20
  97 for @{ 'dpair ${default
  98   @{\lambda ${ident i} : $ty. $p}
  99   @{\lambda ${ident i} . $p}}}.
 100 *)
 101
 102 notation > "𝚺 list1 ident x sep , opt (: T). term 19 Px"
 103   with precedence 20
 104   for ${ default
 105           @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}:$T.$acc)} } }
 106           @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}.$acc)} } }
 107        }.
 108
 109 notation "hvbox(❬ term 19 a, break term 19 b❭)"
 110 with precedence 90 for @{ 'mk_DPair $a $b }.
 111 *)
 112
 113 (* equality, conguence ******************************************************)
 114
 115 notation > "hvbox(a break = b)"
 116   non associative with precedence 45
 117 for @{ 'eq ? $a $b }.
 118
 119 notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
 120   non associative with precedence 45
 121 for @{ 'eq $t $a $b }.
 122
 123 notation > "hvbox(n break ≅ m)"
 124   non associative with precedence 45
 125 for @{ 'congruent $n $m ? }.
 126
 127 notation < "hvbox(term 46 n break ≅ _ term 90 p term 46 m)"
 128   non associative with precedence 45
 129 for @{ 'congruent $n $m $p }.
 130
 131 notation "hvbox(n break ≡ m)"
 132   non associative with precedence 45
 133 for @{ 'equiv $n $m }.
 134
 135 (*
 136 (* other notations **********************************************************)
 137
 138 notation "hvbox(x break \times y)" with precedence 70
 139 for @{ 'product $x $y}.
 140
 141 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
 142 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
 143
 144 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
 145 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
 146
 147 notation > "\fst" with precedence 90 for @{'pi1}.
 148 notation > "\snd" with precedence 90 for @{'pi2}.
 149 *)
 150
 151 notation "hvbox(a break \to b)"
 152   right associative with precedence 20
 153 for @{ \forall $_:$a.$b }.
 154
 155 notation < "hvbox(a break \to b)"
 156   right associative with precedence 20
 157 for @{ \Pi $_:$a.$b }.
 158
 159 (*
 160 notation "hvbox(a break \leq b)"
 161   non associative with precedence 45
 162 for @{ 'leq $a $b }.
 163
 164 notation "hvbox(a break \geq b)"
 165   non associative with precedence 45
 166 for @{ 'geq $a $b }.
 167
 168 notation "hvbox(a break \lt b)"
 169   non associative with precedence 45
 170 for @{ 'lt $a $b }.
 171
 172 notation "hvbox(a break \gt b)"
 173   non associative with precedence 45
 174 for @{ 'gt $a $b }.
 175
 176 notation > "hvbox(a break \neq b)"
 177   non associative with precedence 45
 178 for @{ 'neq ? $a $b }.
 179
 180 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
 181   non associative with precedence 45
 182 for @{ 'neq $t $a $b }.
 183
 184 notation "hvbox(a break \nleq b)"
 185   non associative with precedence 45
 186 for @{ 'nleq $a $b }.
 187
 188 notation "hvbox(a break \ngeq b)"
 189   non associative with precedence 45
 190 for @{ 'ngeq $a $b }.
 191
 192 notation "hvbox(a break \nless b)"
 193   non associative with precedence 45
 194 for @{ 'nless $a $b }.
 195
 196 notation "hvbox(a break \ngtr b)"
 197   non associative with precedence 45
 198 for @{ 'ngtr $a $b }.
 199
 200 notation "hvbox(a break \divides b)"
 201   non associative with precedence 45
 202 for @{ 'divides $a $b }.
 203
 204 notation "hvbox(a break \ndivides b)"
 205   non associative with precedence 45
 206 for @{ 'ndivides $a $b }.
 207
 208 notation "hvbox(a break + b)"
 209   left associative with precedence 55
 210 for @{ 'plus $a $b }.
 211
 212 notation "hvbox(a break - b)"
 213   left associative with precedence 55
 214 for @{ 'minus $a $b }.
 215
 216 notation "hvbox(a break * b)"
 217   left associative with precedence 60
 218 for @{ 'times $a $b }.
 219
 220 notation "hvbox(a break \middot b)"
 221   left associative with precedence 60
 222   for @{ 'middot $a $b }.
 223
 224 notation "hvbox(a break \mod b)"
 225   left associative with precedence 60
 226 for @{ 'module $a $b }.
 227
 228 notation < "a \frac b"
 229   non associative with precedence 90
 230 for @{ 'divide $a $b }.
 231
 232 notation "a \over b"
 233   left associative with precedence 60
 234 for @{ 'divide $a $b }.
 235
 236 notation "hvbox(a break / b)"
 237   left associative with precedence 60
 238 for @{ 'divide $a $b }.
 239
 240 notation "- term 65 a" with precedence 65
 241 for @{ 'uminus $a }.
 242
 243 notation "\sqrt a"
 244   non associative with precedence 65
 245 for @{ 'sqrt $a }.
 246
 247 notation "hvbox(a break \lor b)"
 248   left associative with precedence 30
 249 for @{ 'or $a $b }.
 250
 251 notation "hvbox(a break \land b)"
 252   left associative with precedence 35
 253 for @{ 'and $a $b }.
 254
 255 notation "hvbox(\lnot a)"
 256   non associative with precedence 40
 257 for @{ 'not $a }.
 258
 259 notation > "hvbox(a break \liff b)"
 260   left associative with precedence 25
 261 for @{ 'iff $a $b }.
 262
 263 notation "hvbox(a break \leftrightarrow b)"
 264   left associative with precedence 25
 265 for @{ 'iff $a $b }.
 266
 267
 268 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
 269 for @{ 'powerset $A }.
 270 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
 271 for @{ 'powerset $A }.
 272
 273 notation "hvbox(a break ∈ b)" non associative with precedence 45
 274 for @{ 'mem $a $b }.
 275
 276 notation "hvbox(a break ∉ b)" non associative with precedence 45
 277 for @{ 'notmem $a $b }.
 278
 279 notation "hvbox(a break ≬ b)" non associative with precedence 45
 280 for @{ 'overlaps $a $b }. (* \between *)
 281
 282 notation "hvbox(a break ⊆ b)" non associative with precedence 45
 283 for @{ 'subseteq $a $b }. (* \subseteq *)
 284
 285 notation "hvbox(a break ∩ b)" left associative with precedence 60
 286 for @{ 'intersects $a $b }. (* \cap *)
 287
 288 notation "hvbox(a break ∪ b)" left associative with precedence 55
 289 for @{ 'union $a $b }. (* \cup *)
 290
 291 notation "hvbox(a break \approx b)" non associative with precedence 45
 292   for @{ 'napart $a $b}.
 293
 294 notation "hvbox(a break # b)" non associative with precedence 45
 295   for @{ 'apart $a $b}.
 296
 297 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
 298 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
 299 notation > "a ^ term 90 b"  non associative with precedence 75 for @{ 'exp $a $b}.
 300 *)
 301 notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
 302 (*
 303 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
 304
 305 notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
 306
 307 notation "\naturals" non associative with precedence 90 for @{'N}.
 308 notation "\rationals" non associative with precedence 90 for @{'Q}.
 309 notation "\reals" non associative with precedence 90 for @{'R}.
 310 notation "\integers" non associative with precedence 90 for @{'Z}.
 311 notation "\complexes" non associative with precedence 90 for @{'C}.
 312
 313 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
 314
 315 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
 316 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
 317 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
 318 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
 319 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
 320
 321 notation < "maction (mstyle color #ff0000 (…)) (t)"
 322 non associative with precedence 90 for @{'hide $t}.
 323 *)