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(\langle term 19 a, break term 19 b\rangle)"
 139 with precedence 90 for @{ 'pair $a $b}.
 140
 141 notation "hvbox(x break \times y)" with precedence 70
 142 for @{ 'product $x $y}.
 143
 144 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
 145 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
 146
 147 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
 148 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
 149
 150 notation > "\fst" with precedence 90 for @{'pi1}.
 151 notation > "\snd" with precedence 90 for @{'pi2}.
 152 *)
 153
 154 notation "hvbox(a break \to b)"
 155   right associative with precedence 20
 156 for @{ \forall $_:$a.$b }.
 157
 158 notation < "hvbox(a break \to b)"
 159   right associative with precedence 20
 160 for @{ \Pi $_:$a.$b }.
 161
 162 (*
 163 notation "hvbox(a break \leq b)"
 164   non associative with precedence 45
 165 for @{ 'leq $a $b }.
 166
 167 notation "hvbox(a break \geq b)"
 168   non associative with precedence 45
 169 for @{ 'geq $a $b }.
 170
 171 notation "hvbox(a break \lt b)"
 172   non associative with precedence 45
 173 for @{ 'lt $a $b }.
 174
 175 notation "hvbox(a break \gt b)"
 176   non associative with precedence 45
 177 for @{ 'gt $a $b }.
 178
 179 notation > "hvbox(a break \neq b)"
 180   non associative with precedence 45
 181 for @{ 'neq ? $a $b }.
 182
 183 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
 184   non associative with precedence 45
 185 for @{ 'neq $t $a $b }.
 186
 187 notation "hvbox(a break \nleq b)"
 188   non associative with precedence 45
 189 for @{ 'nleq $a $b }.
 190
 191 notation "hvbox(a break \ngeq b)"
 192   non associative with precedence 45
 193 for @{ 'ngeq $a $b }.
 194
 195 notation "hvbox(a break \nless b)"
 196   non associative with precedence 45
 197 for @{ 'nless $a $b }.
 198
 199 notation "hvbox(a break \ngtr b)"
 200   non associative with precedence 45
 201 for @{ 'ngtr $a $b }.
 202
 203 notation "hvbox(a break \divides b)"
 204   non associative with precedence 45
 205 for @{ 'divides $a $b }.
 206
 207 notation "hvbox(a break \ndivides b)"
 208   non associative with precedence 45
 209 for @{ 'ndivides $a $b }.
 210
 211 notation "hvbox(a break + b)"
 212   left associative with precedence 55
 213 for @{ 'plus $a $b }.
 214
 215 notation "hvbox(a break - b)"
 216   left associative with precedence 55
 217 for @{ 'minus $a $b }.
 218
 219 notation "hvbox(a break * b)"
 220   left associative with precedence 60
 221 for @{ 'times $a $b }.
 222
 223 notation "hvbox(a break \middot b)"
 224   left associative with precedence 60
 225   for @{ 'middot $a $b }.
 226
 227 notation "hvbox(a break \mod b)"
 228   left associative with precedence 60
 229 for @{ 'module $a $b }.
 230
 231 notation < "a \frac b"
 232   non associative with precedence 90
 233 for @{ 'divide $a $b }.
 234
 235 notation "a \over b"
 236   left associative with precedence 60
 237 for @{ 'divide $a $b }.
 238
 239 notation "hvbox(a break / b)"
 240   left associative with precedence 60
 241 for @{ 'divide $a $b }.
 242
 243 notation "- term 65 a" with precedence 65
 244 for @{ 'uminus $a }.
 245
 246 notation "\sqrt a"
 247   non associative with precedence 65
 248 for @{ 'sqrt $a }.
 249
 250 notation "hvbox(a break \lor b)"
 251   left associative with precedence 30
 252 for @{ 'or $a $b }.
 253
 254 notation "hvbox(a break \land b)"
 255   left associative with precedence 35
 256 for @{ 'and $a $b }.
 257
 258 notation "hvbox(\lnot a)"
 259   non associative with precedence 40
 260 for @{ 'not $a }.
 261
 262 notation > "hvbox(a break \liff b)"
 263   left associative with precedence 25
 264 for @{ 'iff $a $b }.
 265
 266 notation "hvbox(a break \leftrightarrow b)"
 267   left associative with precedence 25
 268 for @{ 'iff $a $b }.
 269
 270
 271 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
 272 for @{ 'powerset $A }.
 273 notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
 274 for @{ 'powerset $A }.
 275
 276 notation "hvbox(a break ∈ b)" non associative with precedence 45
 277 for @{ 'mem $a $b }.
 278
 279 notation "hvbox(a break ∉ b)" non associative with precedence 45
 280 for @{ 'notmem $a $b }.
 281
 282 notation "hvbox(a break ≬ b)" non associative with precedence 45
 283 for @{ 'overlaps $a $b }. (* \between *)
 284
 285 notation "hvbox(a break ⊆ b)" non associative with precedence 45
 286 for @{ 'subseteq $a $b }. (* \subseteq *)
 287
 288 notation "hvbox(a break ∩ b)" left associative with precedence 60
 289 for @{ 'intersects $a $b }. (* \cap *)
 290
 291 notation "hvbox(a break ∪ b)" left associative with precedence 55
 292 for @{ 'union $a $b }. (* \cup *)
 293
 294 notation "hvbox(a break \approx b)" non associative with precedence 45
 295   for @{ 'napart $a $b}.
 296
 297 notation "hvbox(a break # b)" non associative with precedence 45
 298   for @{ 'apart $a $b}.
 299
 300 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
 301 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
 302 notation > "a ^ term 90 b"  non associative with precedence 75 for @{ 'exp $a $b}.
 303 *)
 304 notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
 305 (*
 306 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
 307
 308 notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
 309
 310 notation "\naturals" non associative with precedence 90 for @{'N}.
 311 notation "\rationals" non associative with precedence 90 for @{'Q}.
 312 notation "\reals" non associative with precedence 90 for @{'R}.
 313 notation "\integers" non associative with precedence 90 for @{'Z}.
 314 notation "\complexes" non associative with precedence 90 for @{'C}.
 315
 316 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
 317
 318 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
 319 notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
 320 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
 321 notation > "⊩ " with precedence 65 for @{'Vdash ?}.
 322 notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
 323
 324 notation < "maction (mstyle color #ff0000 (…)) (t)"
 325 non associative with precedence 90 for @{'hide $t}.
 326 *)