helm/software/matita/core_notation.moo

   1 (* exists *******************************************************************)
   2
   3 notation "hvbox(∃ _ break . p)"
   4  with precedence 20
   5 for @{'exists $p }.
   6
   7 notation < "hvbox(\exists ident i : ty break . p)"
   8  right associative with precedence 20
   9 for @{'exists (\lambda ${ident i} : $ty. $p) }.
  10
  11 notation < "hvbox(\exists ident i break . p)"
  12   with precedence 20
  13 for @{'exists (\lambda ${ident i}. $p) }.
  14
  15 (*
  16 notation < "hvbox(\exists ident i opt (: ty) break . p)"
  17   right associative with precedence 20
  18 for @{ 'exists ${default
  19   @{\lambda ${ident i} : $ty. $p}
  20   @{\lambda ${ident i} . $p}}}.
  21 *)
  22
  23 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
  24   with precedence 20
  25   for ${ default
  26           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
  27           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
  28        }.
  29
  30 (* sigma ********************************************************************)
  31
  32 notation < "hvbox(\Sigma ident i : ty break . p)"
  33  left associative with precedence 20
  34 for @{'sigma (\lambda ${ident i} : $ty. $p) }.
  35
  36 notation < "hvbox(\Sigma ident i break . p)"
  37  with precedence 20
  38 for @{'sigma (\lambda ${ident i}. $p) }.
  39
  40 (*
  41 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
  42   right associative with precedence 20
  43 for @{ 'sigma ${default
  44   @{\lambda ${ident i} : $ty. $p}
  45   @{\lambda ${ident i} . $p}}}.
  46 *)
  47
  48 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
  49   with precedence 20
  50   for ${ default
  51           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
  52           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
  53        }.
  54
  55 (* other notations **********************************************************)
  56
  57 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
  58 with precedence 90 for @{ 'pair $a $b}.
  59
  60 notation "hvbox(x break \times y)" with precedence 70
  61 for @{ 'product $x $y}.
  62
  63 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
  64 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
  65
  66 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
  67 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
  68
  69 notation > "\fst" with precedence 90 for @{'pi1}.
  70 notation > "\snd" with precedence 90 for @{'pi2}.
  71
  72 notation "hvbox(a break \to b)"
  73   right associative with precedence 20
  74 for @{ \forall $_:$a.$b }.
  75
  76 notation < "hvbox(a break \to b)"
  77   right associative with precedence 20
  78 for @{ \Pi $_:$a.$b }.
  79
  80 notation > "hvbox(a break = b)"
  81   non associative with precedence 45
  82 for @{ 'eq ? $a $b }.
  83 notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
  84   non associative with precedence 45
  85 for @{ 'eq $t $a $b }.
  86
  87 notation "hvbox(a break \leq b)"
  88   non associative with precedence 45
  89 for @{ 'leq $a $b }.
  90
  91 notation "hvbox(a break \geq b)"
  92   non associative with precedence 45
  93 for @{ 'geq $a $b }.
  94
  95 notation "hvbox(a break \lt b)"
  96   non associative with precedence 45
  97 for @{ 'lt $a $b }.
  98
  99 notation "hvbox(a break \gt b)"
 100   non associative with precedence 45
 101 for @{ 'gt $a $b }.
 102
 103 notation > "hvbox(a break \neq b)"
 104   non associative with precedence 45
 105 for @{ 'neq ? $a $b }.
 106
 107 notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
 108   non associative with precedence 45
 109 for @{ 'neq $t $a $b }.
 110
 111 notation "hvbox(a break \nleq b)"
 112   non associative with precedence 45
 113 for @{ 'nleq $a $b }.
 114
 115 notation "hvbox(a break \ngeq b)"
 116   non associative with precedence 45
 117 for @{ 'ngeq $a $b }.
 118
 119 notation "hvbox(a break \nless b)"
 120   non associative with precedence 45
 121 for @{ 'nless $a $b }.
 122
 123 notation "hvbox(a break \ngtr b)"
 124   non associative with precedence 45
 125 for @{ 'ngtr $a $b }.
 126
 127 notation "hvbox(a break \divides b)"
 128   non associative with precedence 45
 129 for @{ 'divides $a $b }.
 130
 131 notation "hvbox(a break \ndivides b)"
 132   non associative with precedence 45
 133 for @{ 'ndivides $a $b }.
 134
 135 notation "hvbox(a break + b)"
 136   left associative with precedence 50
 137 for @{ 'plus $a $b }.
 138
 139 notation "hvbox(a break - b)"
 140   left associative with precedence 50
 141 for @{ 'minus $a $b }.
 142
 143 notation "hvbox(a break * b)"
 144   left associative with precedence 55
 145 for @{ 'times $a $b }.
 146
 147 notation "hvbox(a break \middot b)"
 148   left associative with precedence 55
 149   for @{ 'middot $a $b }.
 150
 151 notation "hvbox(a break \mod b)"
 152   left associative with precedence 55
 153 for @{ 'module $a $b }.
 154
 155 notation "a \frac b"
 156   non associative with precedence 90
 157 for @{ 'divide $a $b }.
 158
 159 notation "a \over b"
 160   left associative with precedence 55
 161 for @{ 'divide $a $b }.
 162
 163 notation "hvbox(a break / b)"
 164   left associative with precedence 55
 165 for @{ 'divide $a $b }.
 166
 167 notation "- term 60 a" with precedence 60
 168 for @{ 'uminus $a }.
 169
 170 notation "a !"
 171   non associative with precedence 80
 172 for @{ 'fact $a }.
 173
 174 notation "\sqrt a"
 175   non associative with precedence 60
 176 for @{ 'sqrt $a }.
 177
 178 notation "hvbox(a break \lor b)"
 179   left associative with precedence 30
 180 for @{ 'or $a $b }.
 181
 182 notation "hvbox(a break \land b)"
 183   left associative with precedence 35
 184 for @{ 'and $a $b }.
 185
 186 notation "hvbox(\lnot a)"
 187   non associative with precedence 40
 188 for @{ 'not $a }.
 189
 190 notation > "hvbox(a break \liff b)"
 191   left associative with precedence 25
 192 for @{ 'iff $a $b }.
 193
 194 notation "hvbox(a break \leftrightarrow b)"
 195   left associative with precedence 25
 196 for @{ 'iff $a $b }.
 197
 198
 199 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
 200 for @{ 'powerset $A }.
 201
 202 notation < "hvbox({ ident i | term 19 p })" with precedence 90
 203 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
 204
 205 notation > "hvbox({ ident i | term 19 p })" with precedence 90
 206 for @{ 'subset (\lambda ${ident i}. $p)}.
 207
 208 notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
 209 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
 210
 211 notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
 212 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
 213
 214 notation "hvbox(a break ∈ b)" non associative with precedence 45
 215 for @{ 'mem $a $b }.
 216
 217 notation "hvbox(a break ≬ b)" non associative with precedence 45
 218 for @{ 'overlaps $a $b }. (* \between *)
 219
 220 notation "hvbox(a break ⊆ b)" non associative with precedence 45
 221 for @{ 'subseteq $a $b }. (* \subseteq *)
 222
 223 notation "hvbox(a break ∩ b)" non associative with precedence 55
 224 for @{ 'intersects $a $b }. (* \cap *)
 225
 226 notation "hvbox(a break ∪ b)" non associative with precedence 50
 227 for @{ 'union $a $b }. (* \cup *)
 228
 229 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
 230
 231 notation "hvbox(a break \approx b)" non associative with precedence 45
 232   for @{ 'napart $a $b}.
 233
 234 notation "hvbox(a break # b)" non associative with precedence 45
 235   for @{ 'apart $a $b}.
 236
 237 notation "hvbox(a break \circ b)"
 238   left associative with precedence 55
 239 for @{ 'compose $a $b }.
 240
 241 notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
 242 notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
 243
 244 notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
 245
 246 notation "↑a" with precedence 55 for @{ 'uparrow $a }.
 247
 248 notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
 249
 250 notation "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}.
 251 notation > "a ^ term 89 b"  with precedence 90 for @{ 'exp $a $b}.
 252 notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }.
 253 notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }.
 254 notation < "s \sup (-1) x" with precedence 90 for @{ 'invert_appl $s $x}.
 255
 256 notation "hvbox(|term 90 C|)" with precedence 69 for @{ 'card $C }.
 257
 258 notation "\naturals" non associative with precedence 90 for @{'N}.
 259 notation "\rationals" non associative with precedence 90 for @{'Q}.
 260 notation "\reals" non associative with precedence 90 for @{'R}.
 261 notation "\integers" non associative with precedence 90 for @{'Z}.
 262 notation "\complexes" non associative with precedence 90 for @{'C}.
 263
 264 notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
 265
 266 notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
 267 notation > "x ⊩_term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
 268 notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
 269 notation > "⊩ " with precedence 60 for @{'Vdash ?}.
 270 notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
 271
 272 notation < "maction (mstyle color #ff0000 (…)) (t)"
 273 non associative with precedence 90 for @{'hide $t}.
 274