Add break hints to =, ==, $==, $->

[Alizter]

We should add break hints to =, ==, $==, $->, $o, $@ and probably many others so that

f $o g

is formatted:

f
$o g

when forced to break. This will make large goals easier to read.

[Alizter]

This should be relatively straightforward to do, I would suggest any potential PR to give an example of goals in the library where reading becomes easier. Examples would probably come from anywhere we have long path algebra.

To give some hints on how to proceed and how the format mechanism works, have a look at:

format "'[v' '[v' f ']' '/' $== '/' '[v' g ']' '/' :> '[' A ']' ']'"

which is for formatting the notation f $== g :> A. Here is what is going on:

1. The outer '[v' and ']' brackets create what is called a "vertical box", this means that the formatter will try to insert new lines every time there is a break hint. This ends up with the contents of the box being "stretched vertically". An example would be:

A \
B \
C

rather than

A \ B \ C

2. The '\' symbols are the break hints, depending on which box they appear in, the formatter will treat them as breaks or not depending on several factors. This generally includes fitting as much as possible on a line until it hits the margin.

3. The '[' and ']' symbols indicate a normal box, which doesn't insert new lines at break hints unless there is no space left within the margin.

For more information about how formatting works, take a look at the OCaml formatting guide. The Coq formatter is based on the OCaml one under the hood.