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