+(* 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〛)"
+ 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}.