matita/matita/contribs/mf/notations.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 notation "hvbox(a break \to b)"
   4  right associative with precedence 20
   5  for @{ \forall $_:$a.$b }.
   6
   7 notation < "hvbox(Σ ident i : ty break . p)"
   8  left associative with precedence 20
   9 for @{'sigma (λ${ident i}: $ty. $p) }.
  10 notation < "hvbox(Σ ident i break . p)"
  11  with precedence 20
  12 for @{'sigma (λ${ident i}. $p) }.
  13
  14 notation > "Σ list1 ident x sep , opt (: T). term 19 Px"
  15   with precedence 20
  16   for ${ default
  17           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}: $T. $acc)} } }
  18           @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}. $acc)} } }
  19        }.
  20
  21 notation "hvbox(π1 s)"
  22  non associative with precedence 70
  23  for @{ 'sig1 $s) }.
  24 notation "hvbox(π2 s)"
  25  non associative with precedence 70
  26  for @{ 'sig2 $s) }.
  27
  28 notation "hvbox(〈 term 19 a, break term 19 b 〉)"
  29  with precedence 90 for @{ 'mk_sigma $a $b }.
  30
  31 notation "hvbox(B break × C)"
  32  left associative with precedence 55
  33  for @{ 'times $B $C }.
  34
  35 notation "⋆"
  36  non associative with precedence 90
  37  for @{ 'star }.
  38
  39 notation "ϵ"
  40  non associative with precedence 90
  41  for @{ 'epsilon }.
  42 notation "⌈ l, c ⌉"
  43  non associative with precedence 90
  44  for @{ 'cons $l $c }.
  45
  46 notation "hvbox(B break + C)"
  47  left associative with precedence 50
  48  for @{ 'plus $B $C }.
  49
  50 notation "⊥"
  51  non associative with precedence 90
  52  for @{ 'falsum }.
  53
  54 notation "hvbox(B break ∨ C)"
  55  left associative with precedence 50
  56  for @{ 'disj $B $C }.
  57
  58 notation "hvbox(B break ∧ C)"
  59  left associative with precedence 60
  60  for @{ 'conj $B $C }.
  61
  62 notation < "hvbox(B break → C)"
  63  left associative with precedence 60
  64  for @{ 'implies $B $C }.
  65
  66 notation < "hvbox(∃ ident i : ty break . p)"
  67  left associative with precedence 20
  68 for @{'exists (λ${ident i}: $ty. $p) }.
  69 notation < "hvbox(∃ ident i break . p)"
  70  with precedence 20
  71 for @{'exists (λ${ident i}. $p) }.
  72
  73 notation > "∃ list1 ident x sep , opt (: T). term 19 Px"
  74   with precedence 20
  75   for ${ default
  76           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}: $T. $acc)} } }
  77           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}. $acc)} } }
  78        }.
  79 notation "hvbox(« term 19 a, break term 19 b »)"
  80  with precedence 90 for @{ 'mk_exists $a $b }.
  81
  82 notation "⊤"
  83  non associative with precedence 90
  84  for @{ 'verum }.
  85
  86 notation "hvbox(a break = b)"
  87  non associative with precedence 45
  88  for @{ 'id $a $b }.
  89
  90 notation "hvbox(a break ≃ b)"
  91  non associative with precedence 45
  92  for @{ 'eq $a $b }.
  93
  94 notation "hvbox(ı x)"
  95  non associative with precedence 90
  96  for @{ 'rfl $x }.
  97 notation "hvbox(d⁻¹)"
  98  non associative with precedence 80
  99  for @{ 'sym $d }.
 100 notation "hvbox(d break • d')"
 101  left associative with precedence 60
 102  for @{ 'tra $d $d' }.
 103
 104 notation "hvbox(y break ∘ d)"
 105  non associative with precedence 50
 106  for @{ 'subst $d $y }.
 107
 108 notation "hvbox(f ◽ d)"
 109  non associative with precedence 40
 110  for @{ 'ap $f $d}.
 111 notation "hvbox(f ˙ d)"
 112  non associative with precedence 60
 113  for @{ 'sup_f $f $d}.
 114