Zulip Chat Archive

Stream: general

Topic: proving quot.mk equality

Bernd Losert (Dec 24 2021 at 14:03):

How does you usually prove an equality like quot.mk r x = quot.mk r y. I see there is a theorem quot.eq, so I guess I need to produce a value of type eqv_gen r x y?

Anne Baanen (Dec 24 2021 at 14:06):

That would be the most general way to do it: eqv_gen r means "the equivalence relation generated by r, so it also works if r is not an equivalence relation. If it is an equivalence relation, then you can use docs#quotient.sound (or docs#quotient.sound' if the instance parameters annoy you)

Bernd Losert (Dec 24 2021 at 14:09):

Cool. Thanks.

Last updated: Aug 03 2023 at 10:10 UTC