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