Re: [isabelle] transfer / lifting / quotient - questions
On 06/23/2014 02:41 PM, Salomon Sickert wrote:
datatype tree = leaf "nat"
| node "tree" "tree"
If I try to generalize nat to 'a, I get the following error from the
Generation of a parametrized correspondence relation failed.
No relator for the type "QuotientTypeTests.tree"
Looking at the quotient examples didn't help me to figure out, what
to prove or define to fix this.
What do I have to do? Or can I simply ignore it?
First of all, it's not an error but a warning. You can ignore it if you
don't want to nest your types during lifting (and transfer), for
example, when you don't want to work with "'a tree tree". If you want to
work with such types (or want to remove the warning for esthetic
reasons), then you have to provide a certain structure to your type. See
for example HOL/Lifting_Option: in the most general case, you need all
the corresponding theorems from the section "Relator and predicator
properties" and "Quotient theorem for the Lifting package".
Note that in the coming release - Isabelle 2014 (released hopefully this
summer) - all these theorems are proved (and registred) automatically
if you define your type with datatype_new.
The other two question don't have probably much to do with Lifting and
Transfer. Mayber more knowledgeable experts can comment on them.
This archive was generated by a fusion of
Pipermail (Mailman edition) and