matita/matita/lib/lambda/background/notation.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* GENERIC NOTATION *********************************************************)
  16
  17 (* Note: this should go to core_notation *)
  18 notation "⊥"
  19   non associative with precedence 90
  20   for @{'false}.
  21
  22 (* Note: this should go to core_notation *)
  23 notation "⊤"
  24   non associative with precedence 90
  25   for @{'true}.
  26
  27 (* Note: this should go to core_notation *)
  28 notation "hvbox(a break ≺ b)"
  29    non associative with precedence 45
  30    for @{ 'prec $a $b }.
  31
  32 notation "hvbox( # term 90 i )"
  33  non associative with precedence 46
  34  for @{ 'VariableReferenceByIndex $i }.
  35
  36 notation "hvbox( { term 46 b } # break term 90 i )"
  37  non associative with precedence 46
  38  for @{ 'VariableReferenceByIndex $b $i }.
  39
  40 notation "hvbox( 𝛌 . term 46 A )"
  41    non associative with precedence 46
  42    for @{ 'Abstraction $A }.
  43
  44 notation "hvbox( { term 46 b } 𝛌 . break term 46 T)"
  45    non associative with precedence 46
  46    for @{ 'Abstraction $b $T }.
  47
  48 notation "hvbox( 𝛌 term 46 d . break term 46 A )"
  49    non associative with precedence 46
  50    for @{ 'AnnotatedAbstraction $d $A }.
  51
  52 notation "hvbox( @ term 46 C . break term 46 A )"
  53    non associative with precedence 46
  54    for @{ 'Application $C $A }.
  55
  56 notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
  57    non associative with precedence 46
  58    for @{ 'Application $b $V $T }.
  59
  60 notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )"
  61    non associative with precedence 46
  62    for @{ 'Lift $h $d $M }.
  63
  64 notation > "hvbox( ↑ [ term 46 h ] break term 46 M )"
  65    non associative with precedence 46
  66    for @{ 'Lift $h 0 $M }.
  67
  68 notation > "hvbox( ↑ term 46 M )"
  69    non associative with precedence 46
  70    for @{ 'Lift 1 0 $M }.
  71
  72 (* Note: the notation with "/" does not work *)
  73 notation "hvbox( [ term 46 d break ↙ term 46 N ] break term 46 M )"
  74    non associative with precedence 46
  75    for @{ 'DSubst $N $d $M }.
  76
  77 notation > "hvbox( [ ↙ term 46 N ] break term 46 M )"
  78    non associative with precedence 46
  79    for @{ 'DSubst $N 0 $M }.
  80
  81 (* Note: we do not use → since it is reserved by CIC *)
  82 notation "hvbox( M break ↦ term 46 N )"
  83    non associative with precedence 45
  84    for @{ 'SeqRed $M $N }.
  85
  86 notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )"
  87    non associative with precedence 45
  88    for @{ 'SeqRed $M $p $N }.
  89
  90 notation "hvbox( M break ↦* term 46 N )"
  91    non associative with precedence 45
  92    for @{ 'SeqRedStar $M $N }.
  93
  94 notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
  95    non associative with precedence 45
  96    for @{ 'SeqRedStar $M $s $N }.
  97
  98 notation "hvbox( M break ⤇ term 46 N )"
  99    non associative with precedence 45
 100    for @{ 'ParRed $M $N }.
 101
 102 notation "hvbox( M break ⤇* term 46 N )"
 103    non associative with precedence 45
 104    for @{ 'ParRedStar $M $N }.