(* *)
(**************************************************************************)
-(* 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(ã\80\9aterm 90 Tã\80\9b)"
+notation "hvbox(ã\80\8aTã\80\8b 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}.