On 11/29/2011 06:21 AM, 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.
The idea of using the quotient package with partial equivalence relations
is that two changes need to be done:
First if the user specifies 'partial:' in the quotient_type definition,
the obligation to prove changes from 'equivp' to 'part_equivp'. Which
is simpler,
but then less lifting can be done automatically (to be more precise, some
of the theorems that allow for automatic regularization do hold only for
reflexive equivalence relations).
Hi Cezary,
could you add this explanation for the partial option to the existing
IsarRef documentation of quotient types to make sure that this piece of
knowledge is not just archived here?
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
