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