- lambda_notation.ma: more notation and bug fixes

[helm.git] / matita / matita / lib / lambda / lambda_notation.ma

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 26185019a6653cecf97dd1a5fbf4cb2860868d18..a5fb014ed7d284cc6cc493bd969c351baa297ef6 100644 (file)
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -34,32 +34,62 @@ notation "hbox((! ^ term 90 b) term 50 a)"
 
 (* 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}.
+
+(* 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}.
 
-(* interpretation *)
+(* interpretations *)
 
-notation "hvbox(〚term 90 T〛)"
+notation "hvbox(║T║)"
    non associative with precedence 50
    for @{'IInt $T}.
 
-notation "hvbox(〚term 90 T〛 break _ [term 90 E])"
+notation "hvbox(║T║ break _ [E])"
    non associative with precedence 50
    for @{'IInt1 $T $E}.
 
-notation "hvbox(〚term 90 T〛 break _ [term 90 E1 break , term 90 E2])"
+notation "hvbox(║T║ break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'IInt2 $T $E1 $E2}.
 
-notation "hvbox(ã\80\8aterm 90 Tã\80\8b)"
+notation "hvbox(ã\80\9aTã\80\9b)"
    non associative with precedence 50
    for @{'EInt $T}.
 
-notation "hvbox(ã\80\8aterm 90 Tã\80\8b break _ [term 90 E])"
+notation "hvbox(ã\80\9aTã\80\9b break _ [E])"
    non associative with precedence 50
    for @{'EInt1 $T $E}.
 
-notation "hvbox(ã\80\8aterm 90 Tã\80\8b break _ [term 90 E1 break , term 90 E2])"
+notation "hvbox(ã\80\9aTã\80\9b 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(《T》 break _ [E1 break , E2])"
+   non associative with precedence 50
+   for @{'XInt2 $T $E1 $E2}.