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



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





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