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 >> (<http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml>), >> 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. Cheers, René 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.
Description: Message signed with OpenPGP using GPGMail