Re: [isabelle] primrec_new error: extra vars on RHS, option return type works



Hi Gottfried, Andreas,

> This looks like a primrec_new bug in Isabelle2013-2 (it works with "the" development version, e.g., 761e40ce91bc). As a workaround, you can wrap x in some function such as id.
> 
> primrec_new get_hS_FAILS :: "hD => hD fset" where
>  "get_hS_FAILS hEM    = {||}"
> |"get_hS_FAILS (hS x) = id x"

Thanks, Andreas, for investigating this.

I would like to add that "primrec_new" and "primcorec" were developed following their own schedule, irrespective of any releases. It turned out that "primrec_new" was more or less finished whereas "primcorec" was a huge construction yard at the time of the Isabelle2013-1/2 releases, something we acknowledged in the documentation ("isabelle doc datatypes"). Hence, expect to run into more issues, at least until the next release.

Incidentally, I'm wondering whether you really need the "hEM" constructor in

    datatype_new hD = hEM | hS "hD fset"

The canonical definition of hereditarily finite sets reads

    datatype_new hD = hS "hD fset"

Regards,

Jasmin





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