X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=8063634d0a3210410d4c98ed31b1dcfae41bb3dd;hb=2343da541bb828ac61079d7811c0fe5613b04fb6;hp=55a75eb780ea28e6010d5c2c050474cb29458f18;hpb=87d894fbd1d1c6ae4f9a8421ffa39af838b72e9f;p=helm.git

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 55a75eb78..8063634d0 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -12,24 +12,95 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
+(* NOTATION FOR THE LAMBDA CALCULUS *)
+(* equivalence, invariance *)
+
+notation "hvbox(a break ≅ b)" 
+  non associative with precedence 45
+  for @{'Eq $a $b}.
+
+notation "hvbox(a break (≅ ^ term 90 c) b)"
+  non associative with precedence 45
+  for @{'Eq1 $c $a $b}.
+
+notation "hbox(! term 50 a)"
+  non associative with precedence 50
+  for @{'Invariant $a}.
+
+notation "hbox((! ^ term 90 b) term 50 a)"
+  non associative with precedence 50
+  for @{'Invariant1 $a $b}.
 
 (* lifting, substitution *)
 
-notation "hvbox(M break [ l ])"
+notation "hvbox(↑ [ p break , k ] break t)"
+   non associative with precedence 50
+   for @{'Lift1 $p $k $t}.
+
+notation "hvbox(M break [ / l ])"
+   non associative with precedence 90
+   for @{'Subst $M $l}.
+
+notation "hvbox(M break [ k ≝ N ])" 
    non associative with precedence 90
-   for @{'Subst1 $M $l}.
+   for @{'Subst1 $M $k $N}.
 
-(* evaluation, interpretation *)
+(* type judgements *)
+
+notation "hvbox(G break  ⊢ A break : B)"
+   non associative with precedence 45
+   for @{'TJ $G $A $B}.
+
+notation "hvbox(G break  ⊢ A break ÷ B)"
+   non associative with precedence 45
+   for @{'TJ0 $G $A $B}.
+
+(* interpretations *)
+
+notation "hvbox(║T║)"
+   non associative with precedence 50
+   for @{'IInt $T}.
+
+notation "hvbox(║T║ break _ [E])"
+   non associative with precedence 50
+   for @{'IInt1 $T $E}.
+
+notation "hvbox(║T║ break _ [E1 break , E2])"
+   non associative with precedence 50
+   for @{'IInt2 $T $E1 $E2}.
+
+notation "hvbox(║T║ * break _ [E])"
+   non associative with precedence 50
+   for @{'IIntS1 $T $E}.
+
+notation "hvbox(〚T〛)"
+   non associative with precedence 50
+   for @{'EInt $T}.
+
+notation "hvbox(〚T〛 break _ [E])"
+   non associative with precedence 50
+   for @{'EInt1 $T $E}.
+
+notation "hvbox(〚T〛 break _ [E1 break , E2])"
+   non associative with precedence 50
+   for @{'EInt2 $T $E1 $E2}.
+
+notation "hvbox(《T》)"
+   non associative with precedence 50
+   for @{'XInt $T}.
+
+notation "hvbox(《T》 break _ [E])"
+   non associative with precedence 50
+   for @{'XInt1 $T $E}.
 
-notation "hvbox(〚term 90 T〛)"
+notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
-   for @{'Eval $T}.
+   for @{'XInt2 $T $E1 $E2}.
 
-notation "hvbox(〚term 90 T〛 break _ [term 90 E])"
+notation "hvbox(𝕂{G})"
    non associative with precedence 50
-   for @{'Eval1 $T $E}.
+   for @{'IK $G}.
 
-notation "hvbox(〚term 90 T〛 break _ [term 90 E1 break , term 90 E2])"
+notation "hvbox(𝕂{T} break _ [G])"
    non associative with precedence 50
-   for @{'Eval2 $T $E1 $E2}.
+   for @{'IK $T $G}.