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