Re: [isabelle] primcorec complains about invalid map function
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.
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.)
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
interpretation sum_datatype_new .
primcorec bbind ...
> (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. ;)
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.
All right: Thanks for your patience and for taking the time to file in the bug report!
Thanks for fixing all this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and