sets from quotients

Stream: general

[Chris Hughes]

Sets from quotients. Is there a function in lean which basically gives me this {a : α // setoid.r (quot.out x) a}. Also is there any tutorial anywhere on how things like heq, eq.dcases_on, eq.rec_on etc work?

[Andrew Ashworth]

you need to fire up your Coq installation and read http://adam.chlipala.net/cpdt/html/Equality.html :|

[Simon Hudon]

Once you've learned about them, feel free to write a Lean documentation for them

[Chris Hughes]

What I've discovered is typing induction h where h is the proof that the types are equal, help to solve heq goals very easily

[Patrick Massot]

Yes, you're in the right mindset now! You can go and write some doc

[Mario Carneiro]

This can also be expressed as {a // ⟦a⟧ = x}

[Chris Hughes]

I just realised that. Probably more sensible.