left associative with precedence 49
for @{ 'DxAbst $T1 $T2 }.
-notation "hvbox( T . break โฃ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )"
- non associative with precedence 50
- for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
-
notation "hvbox( โฏ { term 46 x } )"
non associative with precedence 90
for @{ 'Weight $x }.
non associative with precedence 45
for @{ 'Simple $T }.
-notation "hvbox( L โข break term 46 T1 โ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'Hom $L $T1 $T2 }.
-
notation "hvbox( T1 โ break term 46 T2 )"
non associative with precedence 45
for @{ 'Iso $T1 $T2 }.
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
-notation "hvbox( L1 break โ [ term 46 d , break term 46 e ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'SubEq $L1 $d $e $L2 }.
-
-notation "hvbox( โ [ term 46 d , break term 46 e ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'SubEqBottom $d $e $L2 }.
-
notation "hvbox( โฉ [ term 46 e ] break term 46 L1 โก break term 46 L2 )"
non associative with precedence 45
for @{ 'RDrop $e $L1 $L2 }.
non associative with precedence 45
for @{ 'SupTermStar $L1 $T1 $L2 $T2 }.
+notation "hvbox( L1 โ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'SubEq $L1 $L2 }.
+
notation "hvbox( L โข break term 46 T1 โถ* break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $L $T1 $T2 }.
non associative with precedence 45
for @{ 'Normal $L $T }.
-(* this might be removed *)
-notation "hvbox( ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L โข break ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'NotHdReducible $T }.
-
-(* this might be removed *)
-notation "hvbox( L โข break ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'NotHdReducible $L $T }.
-
-(* this might be removed *)
-notation "hvbox( ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdNormal $T }.
-
-(* this might be removed *)
-notation "hvbox( L โข break ๐๐ โฆ term 46 T โฆ )"
- non associative with precedence 45
- for @{ 'HdNormal $L $T }.
-
notation "hvbox( L โข break term 46 T1 โก break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
non associative with precedence 45
for @{ 'PRedSnStar $L1 $L2 }.
+notation "hvbox( L1 โข โกโก* break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSnStarAlt $L1 $L2 }.
+
notation "hvbox( L โข break term 46 T1 โก * break ๐ โฆ term 46 T2 โฆ )"
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.