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.

john


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.

Ondrej





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