Re: [isabelle] primcorec complains about invalid map function



Hi Andreas,

Am 06.02.2014 um 09:44 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

> It would be nice if such basic type constructors like sum and product work with prim(co)rec. I tried to register sum with wrap_free_constructors, but that did not work.

Did you specify selectors? Currently (and unfortunately), the tactics behind "primcorec" require types with "sel_split" theorems, which are generated only for types with selectors and discriminators.

> I now have a local sum type as a temporary workaround.

I'll see what I can do. In fact, there's a lot that can and will be done at some point or another, including having us enrich the structure of "list", "option", "sum", and "prod". Today these are BNFs and free constructor types without selectors and discriminators. The next steps are (1) free constructor types with selectors and discriminators; (2) new-style datatypes (either using "datatype_new" or a forthcoming "wrap_datatype_new" command, depending on the type). The latter would allow things like nested-to-mutual recursion through lists.

>> All right: Thanks for your patience and for taking the time to file in the bug report!
> I did not consider this a bug report. I was simply desperate because nothing worked and I thought that I had still not understood how nested corecursion works map functions.

To me, any report of one of my tools spitting out an exception is a bug report. Even though we know that "primcorec" messaging is not finished; see e.g.

https://bitbucket.org/traytel/co-rec/src/2959b88c3f52790b1ab7ada19654a2527bfa1d67/Examples/Primcorec_Messages.thy?at=default

Cheers,

Jasmin





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