non associative with precedence 45
for @{ 'StaticType $h $g $l $L $T1 $T2 }.
+notation "hvbox( h ⊢ break term 46 L1 • ≃ [ g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CCongS $h $g $L1 $L2 }.
+
notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )"
non associative with precedence 45
for @{ 'CrSubEqS $h $g $L1 $L2 }.
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( ⦃ L1 ⦄ ⬌ ⦃ L2 ⦄ )"
+notation "hvbox( ⦃ L1 ⦄ ⬌ break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPConv $L1 $L2 }.
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
+
(* Equivalence **************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )"
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )"
+notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPConvStar $L1 $L2 }.
-notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ * break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ * break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ * break ⦃ L2 , break T2 ⦄ )"
non associative with precedence 45
- for @{ 'CPConvStar $L1 $L2 }.
+ for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
(* Dynamic typing ***********************************************************)