Re: [isabelle] Problem with sort constraints

Dear Andreas,

> Dear René,
> > So my question is, whether this is also possible for class-constraints?
> No. Type classes are explicitly made to prevent applications of overloaded constants when it is not clear that there is an instantiation.

thanks, this was the expected answer, which tells me that I have to do some work.

> I do not see why you need a type class in this case at all. You could equally well define emb_list inside the proof itself and not introduce the type constraint at all:
> Obviously, definitions inside proofs are not as convenient as top-level definitions. You could also define emb_list only for lists and use that, but possibly, your real use case is more complex and you do want to use the global emb.

Exactly, for my presented (short) proof, it is easy to do it within the proof. In the general setting, I'll have to think about how to solve this problem.

> If you want to do overloading without sort constraints, there's the overloading command (Isar-Ref manual 5.8) or the old-fashioned consts+defs (overloaded) pattern, without type classes at all. Note, however, that you then will lose the ability to generate code for whatever is to be implemented in terms of emb. To that end, you would have reintroduce the type class for code generation as follows:

Thanks for the pointers. I'll have a look into it whether these techniques can be utilized to solve my problem.


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