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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
