General precedence rule

[favonia]

The upcoming Agda 4.3 no longer has a default fixity/precedence for operators and syntax (which was infix 20 and infix -666, respectively, I believe). In order to make the current code compile we need to put in many fixity/precedence declarations. I would like to take this opportunity to propose the following general rules for precedence:

1. Separators _$_ and arrows: 0
2. Layout combinators (equational reasoning): 10-15
3. Equalities, equivalences: 30
4. Other relations, operators with line-level separators: 40
5. Constructors (for example _,_): 60
6. Binary operators (including type formers like _×_): 80
7. Prefix operators: 100
8. Postfix operators: 120

Any suggestions or comments?

[andrejbauer]

Yes, multiply all numbers in your list by 10.

[favonia]

I am going to implement this with @andrejbauer's suggestion.