Zulip Chat Archive

Stream: new members

Topic: naming equivalence relation


view this post on Zulip Ali Sever (Jul 18 2018 at 15:52):

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)?

view this post on Zulip Reid Barton (Jul 18 2018 at 15:54):

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

view this post on Zulip Reid Barton (Jul 18 2018 at 15:56):

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

view this post on Zulip Reid Barton (Jul 18 2018 at 15:57):

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

view this post on Zulip Ali Sever (Jul 18 2018 at 16:23):

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

view this post on Zulip Kevin Buzzard (Jul 18 2018 at 16:56):

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?

view this post on Zulip Patrick Massot (Jul 18 2018 at 16:58):

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

view this post on Zulip Reid Barton (Jul 18 2018 at 16:58):

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.

view this post on Zulip Reid Barton (Jul 18 2018 at 16:58):

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

view this post on Zulip Reid Barton (Jul 18 2018 at 17:13):

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).


Last updated: May 11 2021 at 13:22 UTC