(* NOTATION FOR THE "functional" COMPONENT ********************************)
-notation "hvbox( ↑ [ d , break e ] break T )"
- non associative with precedence 55
+notation "hvbox( ↑ [ d , break e ] break term 60 T )"
+ non associative with precedence 60
for @{ 'Lift $d $e $T }.
-notation "hvbox( [ d ← break V ] break T )"
- non associative with precedence 55
+notation "hvbox( [ d ← break V ] break term 60 T )"
+ non associative with precedence 60
for @{ 'Subst $V $d $T }.
-notation "hvbox( T1 ⇨ break T2 )"
+notation "hvbox( T1 ⇨ break term 46 T2 )"
non associative with precedence 45
for @{ 'SRed $T1 $T2 }.