Precedence of infix notation

[mikeshulman]

Why did you choose an infix notation whose precedence is higher than function application? It's contrary to all my intuitions for f x #< y to mean f (x #< y).

[jonsterling]

Wow! I did not realize that there was an operator with such a high precedence... I think we ought to change this. (Or, honestly, just remove the infix operator.)

[favonia]

I have been unhappy with the current symbols, but let me propose something before we throw all infix operators out. :smile_cat:

• <: for "snoc": Emp <: 1 <: 2 <: 3. Previously, it's #<.
• <@ for append: Emp <@ [4; 5; 6] <@ [7; 8; 9]. Previously, it's <><.
• @> for prepend: b1 @> b2 @> [10]. Previously, it's <>>.

Advantages:

1. Their precedence is lower than function application (addressing the current issue): https://v2.ocaml.org/manual/expr.html#ss%3Aprecedence-and-associativity
2. <: and <@ are left-associative and @> is right-associative. Previously, <>> is wrongly left-associative, which means you cannot write b1 <>> b2 <>> .... The proposed replacement of <>>, @>, is correctly right-associative.
3. Visually, <: is close to the built-in list "cons" :: and <@ and @> are close to the built-in list concatenation @. Directions of <@ and @> are clearer than those of <>< and <>>. As a consequence, <: (Snoc) and <@ (append) look more consistent and it's easy to remember <@ (append) and @> (prepend).