matita/matita/lib/lambda/lambda_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 (* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
  16
  17 (* equivalence, invariance *)
  18
  19 notation "hvbox(a break ≅ b)"
  20   non associative with precedence 45
  21   for @{'Eq $a $b}.
  22
  23 notation "hvbox(a break (≅ ^ term 90 c) b)"
  24   non associative with precedence 45
  25   for @{'Eq1 $c $a $b}.
  26
  27 notation "hbox(! term 50 a)"
  28   non associative with precedence 50
  29   for @{'Invariant $a}.
  30
  31 notation "hbox((! ^ term 90 b) term 50 a)"
  32   non associative with precedence 50
  33   for @{'Invariant1 $a $b}.
  34
  35 (* lifting, substitution *)
  36
  37 notation "hvbox(↑ [ p break , k ] break t)"
  38    non associative with precedence 50
  39    for @{'Lift1 $p $k $t}.
  40
  41 notation "hvbox(M break [ / l ])"
  42    non associative with precedence 90
  43    for @{'Subst $M $l}.
  44
  45 notation "hvbox(M break [ k ≝ N ])"
  46    non associative with precedence 90
  47    for @{'Subst1 $M $k $N}.
  48
  49 (* type judgements *)
  50
  51 notation "hvbox(G break  ⊢ A break : B)"
  52    non associative with precedence 45
  53    for @{'TJ $G $A $B}.
  54
  55 notation "hvbox(G break  ⊢ A break ÷ B)"
  56    non associative with precedence 45
  57    for @{'TJ0 $G $A $B}.
  58
  59 (* interpretations *)
  60
  61 notation "hvbox(║T║)"
  62    non associative with precedence 50
  63    for @{'IInt $T}.
  64
  65 notation "hvbox(║T║ break _ [E])"
  66    non associative with precedence 50
  67    for @{'IInt1 $T $E}.
  68
  69 notation "hvbox(║T║ break _ [E1 break , E2])"
  70    non associative with precedence 50
  71    for @{'IInt2 $T $E1 $E2}.
  72
  73 notation "hvbox(〚T〛)"
  74    non associative with precedence 50
  75    for @{'EInt $T}.
  76
  77 notation "hvbox(〚T〛 break _ [E])"
  78    non associative with precedence 50
  79    for @{'EInt1 $T $E}.
  80
  81 notation "hvbox(〚T〛 break _ [E1 break , E2])"
  82    non associative with precedence 50
  83    for @{'EInt2 $T $E1 $E2}.
  84
  85 notation "hvbox(《T》)"
  86    non associative with precedence 50
  87    for @{'XInt $T}.
  88
  89 notation "hvbox(《T》 break _ [E])"
  90    non associative with precedence 50
  91    for @{'XInt1 $T $E}.
  92
  93 notation "hvbox(《T》 break _ [E1 break , E2])"
  94    non associative with precedence 50
  95    for @{'XInt2 $T $E1 $E2}.