Re: [isabelle] primcorec complains about invalid map function



Hi Jasmin,

On 06/02/14 17:15, Jasmin Blanchette wrote:
Ah, that one was easy to fix (a87e49f4336d).
Thanks, my example now also works with wrap_free_constructors. Maybe the wrap_free_constructors declaration could be moved to Sum_Type?

> Incidentally, looking at 062aa11e98e1 in conjunction with a87e49f4336d suggests that some Isabelle developers are like monkeys in front of typewriters. Unfortunately, the DUP exception is back in Isabelle/b5b64d9d1002 as the following example shows (AFP/3daf6a41c65b).

theory Scratch imports
  "$AFP/Coinductive/Coinductive_Nat"
  "~~/src/HOL/Probability/Probability"
begin

*** exception DUP "Extended_Nat.enat" raised (line 374 of "General/table.ML")
*** At command "theory"

Happy debugging,
Andreas




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