naming equivalence relation

Stream: new members

[Ali Sever]

I have a function eqd : point → point → point → point → Prop, and I have made an equivalence relation on point × point. Instead of using setoid.r (a,b) (c,d), is it possible to change the notation to be (a,b) ≡ (c,d)?

[Reid Barton]

Yes.
You can already use ≈ as notation for setoid.r, if you don't mind using that instead.

[Reid Barton]

Otherwise, you can define local infix ≡ := setoid.r, or a number of variations on this.

[Reid Barton]

local is optional, depending on whether you want the notation to be in effect everywhere or only in the current file/section

[Ali Sever]

I'm assuming it's not possible to make the notation a b ≡ c d.

[Kevin Buzzard]

I don't know if the parser can handle that. You want more than an infix operator -- you want an operator which eats two things on both sides. I wonder if (a b ≡ c d) would be possible somehow?

[Patrick Massot]

Depends on your alignment. Chaotic evil players are allowed to use tricky unicode blank characters to achieve what you want.

[Reid Barton]

I don't think you can have two arguments to the notation separated only by whitespace.
The way to test this is to try out things like notation a b ` ≡ ` c d := a + b. That gives an error on b.

[Reid Barton]

Yes, I should have been more careful and specified which sort of whitespace I meant. :)

[Reid Barton]

Another option for the chaotic player is to define a has_coe_to_fun from point to point -> (point, point) which sends a to \lam b, (a, b).