Re: [isabelle] primcorec complains about invalid map function



Hi Andreas,

> I tried the following in Isabelle/8a53ee72e595.
> 
> wrap_free_constructors
>  [Inl, Inr]
>  case_sum
>  [is_Inl, is_Inr]
>  [[projl], [projr]]
> sorry
> 
> primcorec bbind :: "('a, 'c) bar => ('a => ('b, 'c) bar) => ('b, 'c) bar"
> where
>  "un_Bar (bbind r f) =
>   map_foobar (map_foo id (case_sum id (split bbind)))
>     (fbind (un_Bar r)
>      (case_foo
>        (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"

Ah, that one was easy to fix (a87e49f4336d). Incidentally, looking at 062aa11e98e1 in conjunction with a87e49f4336d suggests that some Isabelle developers are like monkeys in front of typewriters.

Cheers,

Jasmin





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