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

Jasmin Blanchette jasmin.blanchette at gmail.com
Thu Feb 13 13:47:41 CET 2014

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?



More information about the isabelle-dev mailing list