Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion

Dear Lars and all,

>> My question is: How to define "count_rose" in such a way that I don't
>> have to repeat large parts of "count_list"?
>> The ultimate goal is to derive these instances automatically. I know
>> about the relevant AFP entry
>> (<>),
>> but as far as I can see, it builds on the old datatype package, and I'd
>> rather like to have something for the new BNF package.

Indeed, currently everything in the AFP-entry Datatype_Order_Generator works via
the interface of the old datatype-package, but most of it is currently 
accessible via datatype_compat (but not "derive countable"). 

It is on my TODO list to adapt the AFP-entry to the new datatype package, but
currently this is not a high-priority item, so it might take some while.


PS: I can only confirm Florian's comment on not using "fun" but primrec instead.
In the first version I tried to develop the order-generators via the function package
which turned out quite to be quite complicated / tedious. Once I switched to the
recursors from the old datatype package, the whole task became much simpler.

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

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