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