[isabelle-dev] Quotient example with partiality?

Makarius makarius at sketis.net
Wed Nov 30 11:13:32 CET 2011


On Tue, 29 Nov 2011, Cezary Kaliszyk wrote:

> When developing the quotient package we included the infrastructure for 
> defining quotient types with partial equivalence relations, however 
> since one of the main uses was supposed to be nominal (where its always 
> reflexive) we did not test the partial functionality too much.

> I will try to draft an example partial quotient and get back to you.

Maybe this really old example of partial equivalence relations and 
typedefs is of some interest, at least as amusement:

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle99/src/HOL/Quot/


 	Makarius




More information about the isabelle-dev mailing list