Re: [isabelle] setup_lifting - "no relator for the type" warning

On 01/23/2013 05:24 PM, John Wickerson wrote:
Dear Isabelle,

My attempt to make a typedef for finite sets ...

typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)

setup_lifting type_definition_fset

... results in the following warning message.

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "Set.set" found.

Could somebody kindly tell me how I can address this? Thanks.


The relator for sets is defined in ~~/src/HOL/Library/Quotient_Set. Including this file should remove the warning.

The warning is currently not really harmful because parametrized correspondence relations are not used in Isabelle2013. I didn't include other improvements of the Lifting package that depends on them to the coming release. Maybe in the next release this will come into play.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.