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