non associative with precedence 45
for @{ 'RDrop $d $e $L1 $L2 }.
+notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
+
notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )"
non associative with precedence 45
for @{ 'ICM $L $T $k }.
non associative with precedence 45
for @{ 'RDropStar $e $L1 $L2 }.
+notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ + break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ * break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'RestSupTermStar $L1 $T1 $L2 $T2 }.
+
notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+notation "hvbox( T1 break ⊢ ▶ * [ d , break e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarSn $T1 $d $e $T2 }.
+
+notation "hvbox( T1 break ⊢ ▶ ▶ * [ d , break e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+
notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
-notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CPRed $L1 $L2 }.
-
notation "hvbox( ⦃ L1 ⦄ ➡ break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPRed $L1 $L2 }.
non associative with precedence 45
for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )"
+notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XPRed $h $g $L $T1 $T2 }.
(* Computation **************************************************************)
-notation "hvbox( T1 ➡* break term 46 T2 )"
+notation "hvbox( T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $T1 $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡* break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
-notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
+notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStarAlt $T1 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ➡ * break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedStar $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , T1 ⦄ ➡ * break ⦃ L2 , T2 ⦄ )"
non associative with precedence 45
- for @{ 'CPRedStar $L1 $L2 }.
+ for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )"
+notation "hvbox( ⦃ L1 ⦄ ➡ ➡ * break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedStarAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , T1 ⦄ ➡ ➡ * break ⦃ L2 , T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )"
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
-notation "hvbox( ⬊ * term 46 T )"
+notation "hvbox( ⬊ * term 46 T )"
non associative with precedence 45
for @{ 'SN $T }.
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
-notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ break term 46 T1 â\9e¸ * break [ g ] break term 46 T2 )"
+notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ break term 46 T1 â\80¢ â\9e¡ * break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XPRedStar $h $g $L $T1 $T2 }.
-notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ â\9e· * break [ g ] break term 46 T2 )"
+notation "hvbox( â¦\83 h , break L â¦\84 â\8a¢ â\80¢ â¬\8a * break [ g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'XSN $h $g $L $T }.
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( T1 ⊢ ⬌ break term 46 T2 )"
+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 @{ 'CPConv $T1 $T2 }.
+ for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
(* Equivalence **************************************************************)
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )"
+notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ g ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'CPConvStar $T1 $T2 }.
+ for @{ 'CrSubEqSE $h $g $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStar $L1 $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 @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
(* Dynamic typing ***********************************************************)
non associative with precedence 45
for @{ 'NativeValid $h $g $L $T }.
+notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqV $h $g $L1 $L2 }.
+
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
non associative with precedence 45
for @{ 'NativeType $h $L $T1 $T2 }.