non associative with precedence 45
for @{ 'RDrop $d $e $L1 $L2 }.
-notation "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )"
+notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ break ⦃ L2 , break T2 ⦄ )"
non associative with precedence 45
- for @{ 'SupTerm $L1 $T1 $L2 $T2 }.
+ for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }.
notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )"
non associative with precedence 45
non associative with precedence 45
for @{ 'RDropStar $e $L1 $L2 }.
-notation "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )"
+notation "hvbox( ⦃ L1, break T1 ⦄ ⧁ + break ⦃ L2 , break T2 ⦄ )"
non associative with precedence 45
- for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
+ 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
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 @{ 'XPRed $h $g $L $T1 $T2 }.
-notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )"
- non associative with precedence 45
- for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }.
-
(* Computation **************************************************************)
notation "hvbox( T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'XSN $h $g $L $T }.
-notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ * break [ g ] break ⦃ L2 , break T2 ⦄ )"
- non associative with precedence 45
- for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )"
- non associative with precedence 45
- for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }.
-
(* Conversion ***************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
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 }.