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