helm/software/matita/core_notation.moo

   1 notation < "hvbox(\exists ident i opt (: ty) break . p)"
   2   right associative with precedence 20
   3 for @{ 'exists ${default
   4   @{\lambda ${ident i} : $ty. $p}
   5   @{\lambda ${ident i} . $p}}}.
   6
   7 notation > "\exists ident x:A.break term 19 Px" with precedence 20 for @{ 'exists (λ${ident x}:$A.$Px) }.
   8
   9 notation > "\exists ident x.break term 19 Px" with precedence 20 for @{ 'exists (λ${ident x}.$Px) }.
  10
  11 notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
  12 with precedence 90 for @{ 'pair $a $b}.
  13
  14 notation "hvbox(x break \times y)" with precedence 70
  15 for @{ 'product $x $y}.
  16
  17 notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
  18 notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
  19
  20 notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
  21 notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
  22
  23 notation > "\fst" with precedence 90 for @{'pi1}.
  24 notation > "\snd" with precedence 90 for @{'pi2}.
  25
  26 notation "hvbox(a break \to b)"
  27   right associative with precedence 20
  28 for @{ \forall $_:$a.$b }.
  29
  30 notation < "hvbox(a break \to b)"
  31   right associative with precedence 20
  32 for @{ \Pi $_:$a.$b }.
  33
  34 notation "hvbox(a break = b)"
  35   non associative with precedence 45
  36 for @{ 'eq $a $b }.
  37
  38 notation "hvbox(a break \leq b)"
  39   non associative with precedence 45
  40 for @{ 'leq $a $b }.
  41
  42 notation "hvbox(a break \geq b)"
  43   non associative with precedence 45
  44 for @{ 'geq $a $b }.
  45
  46 notation "hvbox(a break \lt b)"
  47   non associative with precedence 45
  48 for @{ 'lt $a $b }.
  49
  50 notation "hvbox(a break \gt b)"
  51   non associative with precedence 45
  52 for @{ 'gt $a $b }.
  53
  54 notation "hvbox(a break \neq b)"
  55   non associative with precedence 45
  56 for @{ 'neq $a $b }.
  57
  58 notation "hvbox(a break \nleq b)"
  59   non associative with precedence 45
  60 for @{ 'nleq $a $b }.
  61
  62 notation "hvbox(a break \ngeq b)"
  63   non associative with precedence 45
  64 for @{ 'ngeq $a $b }.
  65
  66 notation "hvbox(a break \nless b)"
  67   non associative with precedence 45
  68 for @{ 'nless $a $b }.
  69
  70 notation "hvbox(a break \ngtr b)"
  71   non associative with precedence 45
  72 for @{ 'ngtr $a $b }.
  73
  74 notation "hvbox(a break \divides b)"
  75   non associative with precedence 45
  76 for @{ 'divides $a $b }.
  77
  78 notation "hvbox(a break \ndivides b)"
  79   non associative with precedence 45
  80 for @{ 'ndivides $a $b }.
  81
  82 notation "hvbox(a break + b)"
  83   left associative with precedence 50
  84 for @{ 'plus $a $b }.
  85
  86 notation "hvbox(a break - b)"
  87   left associative with precedence 50
  88 for @{ 'minus $a $b }.
  89
  90 notation "hvbox(a break * b)"
  91   left associative with precedence 55
  92 for @{ 'times $a $b }.
  93
  94 notation "hvbox(a break \mod b)"
  95   left associative with precedence 55
  96 for @{ 'module $a $b }.
  97
  98 notation "\frac a b"
  99   non associative with precedence 90
 100 for @{ 'divide $a $b }.
 101
 102 notation "a \over b"
 103   left associative with precedence 55
 104 for @{ 'divide $a $b }.
 105
 106 notation "hvbox(a break / b)"
 107   left associative with precedence 55
 108 for @{ 'divide $a $b }.
 109
 110 notation "- term 60 a" with precedence 60
 111 for @{ 'uminus $a }.
 112
 113 notation "a !"
 114   non associative with precedence 80
 115 for @{ 'fact $a }.
 116
 117 notation "(a \sup b)"
 118   right associative with precedence 65
 119 for @{ 'exp $a $b}.
 120
 121 notation "\sqrt a"
 122   non associative with precedence 60
 123 for @{ 'sqrt $a }.
 124
 125 notation "hvbox(a break \lor b)"
 126   left associative with precedence 30
 127 for @{ 'or $a $b }.
 128
 129 notation "hvbox(a break \land b)"
 130   left associative with precedence 35
 131 for @{ 'and $a $b }.
 132
 133 notation "hvbox(\lnot a)"
 134   non associative with precedence 40
 135 for @{ 'not $a }.