matita/matita/contribs/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 "hvbox(a break ≺ b)"
  19    non associative with precedence 45
  20    for @{ 'prec $a $b }.
  21
  22 notation "hvbox( # term 90 i )"
  23  non associative with precedence 46
  24  for @{ 'VariableReferenceByIndex $i }.
  25
  26 notation "hvbox( { term 46 b } # break term 90 i )"
  27  non associative with precedence 46
  28  for @{ 'VariableReferenceByIndex $b $i }.
  29
  30 notation "hvbox( 𝛌  . term 46 A )"
  31    non associative with precedence 46
  32    for @{ 'Abstraction $A }.
  33
  34 notation "hvbox( { term 46 b } 𝛌  . break term 46 T)"
  35    non associative with precedence 46
  36    for @{ 'Abstraction $b $T }.
  37
  38 notation "hvbox( @ term 46 C . break term 46 A )"
  39    non associative with precedence 46
  40    for @{ 'Application $C $A }.
  41
  42 notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
  43    non associative with precedence 46
  44    for @{ 'Application $b $V $T }.
  45
  46 notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )"
  47    non associative with precedence 46
  48    for @{ 'Lift $h $d $M }.
  49
  50 notation > "hvbox( ↑ [ term 46 h ] break term 46 M )"
  51    non associative with precedence 46
  52    for @{ 'Lift $h 0 $M }.
  53
  54 notation > "hvbox( ↑ term 46 M )"
  55    non associative with precedence 46
  56    for @{ 'Lift 1 0 $M }.
  57
  58 (* Note: the notation with "/" does not work *)
  59 notation "hvbox( [ term 46 d break ↙ term 46 N ] break term 46 M )"
  60    non associative with precedence 46
  61    for @{ 'DSubst $N $d $M }.
  62
  63 notation > "hvbox( [ ↙ term 46 N ] break term 46 M )"
  64    non associative with precedence 46
  65    for @{ 'DSubst $N 0 $M }.
  66
  67 (* Note: we do not use → since it is reserved by CIC *)
  68 notation "hvbox( M break ↦ term 46 N )"
  69    non associative with precedence 45
  70    for @{ 'SeqRed $M $N }.
  71
  72 notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )"
  73    non associative with precedence 45
  74    for @{ 'SeqRed $M $p $N }.
  75
  76 notation "hvbox( M break ↦* term 46 N )"
  77    non associative with precedence 45
  78    for @{ 'SeqRedStar $M $N }.
  79
  80 notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
  81    non associative with precedence 45
  82    for @{ 'SeqRedStar $M $s $N }.
  83
  84 notation "hvbox( M break ⤇ term 46 N )"
  85    non associative with precedence 45
  86    for @{ 'ParRed $M $N }.
  87
  88 notation "hvbox( M break ⤇* term 46 N )"
  89    non associative with precedence 45
  90    for @{ 'ParRedStar $M $N }.