Changing the notation for Sym2

Stream: graph theory

[Kyle Miller]

#8729 is a PR to change Sym2 to remove a global Setoid instance, which hasn't been so nice of Sym2 to depend on.

It switches from the ⟦(x, y)⟧ Quotient notation to a custom s(x, y) notation. This has better type inference properties too. The PR turns off ⟦(x, y)⟧ notation completely to avoid Quotient or Quot leaking out of the Sym2 API.

Does anyone who uses the graph theory library have any thoughts about this change?

[Yaël Dillies]

I am happy with it!

[Kyle Miller]

@Bhavik Mehta @Yaël Dillies If we're happy with it, do we want to move forward with merging it?

[Yaël Dillies]

Will have a look later