Re: [isabelle] primcorec complains about invalid map function



Dear Jasmin,

This is currently not supported, because "sum" is an old-style datatype and "primrec" can only deal with new-style "case"s. (It wouldn't be hard to hard-code something for sums and products on our side, though.)
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.
I now have a local sum type as a temporary workaround.

locale sum_datatype_new begin
datatype_new ('a, 'b) sum = Inl 'a | Inr 'b
end
context begin
interpretation sum_datatype_new .
primcorec bbind ...
end

> (In fact, the naming "case_sum" in your example suggests that you are using a new-style datatype, if it's not a typo.) True, I am hooked on the repository version again. But as I had the same problems in Isabelle2013-2, I thought that I post this on isabelle-users for documentation.

> I hope you feel slightly guilty for shaming us [**] publicly like that. ;)

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.

Thanks for fixing all this.

Andreas




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