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.
Did you specify selectors?
I tried the following in Isabelle/8a53ee72e595.
primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
"un_Bar (bbind r f) =
map_foobar (map_foo id (case_sum id (split bbind)))
(fbind (un_Bar r)
(map_foobar (map_foo id Inl) o un_Bar o f)
(%c. AA (B (%i. Inr (c i, f))))))"
It results in the following exception:
*** exception TERM raised (line 366 of "~~/src/HOL/Tools/hologic.ML"):
*** mk_split: bad body type
*** Inr ()
*** At command "primcorec"
This archive was generated by a fusion of
Pipermail (Mailman edition) and