[isabelle-dev] [isabelle] primcorec complains about invalid map function

[Jasmin Blanchette]

Hi Andreas,

Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

> In summary, I do not want to replace "_ = None" and "_ = []" with null and is_none, I'd just like to make null and is_none somewhat official. I am not sure when these discriminators can show up in practice, but I thought that only primcorec needs them. So from my point of view, it seems sensible to make them the official discriminators.

Now I'm confused. If we do what you just proposed, the discriminators end up appearing in some of the generated theorems -- and you observed yourself that "the destructor view is not at all convenient for datatypes, because most functions pattern match on the constructors. Therefore, it is better the have the constructors explicit." For a datatype, being an "official" discriminator basically amounts to "appearing in generated theorems". Or did I misunderstood something?

Cheers,

Jasmin