Hi Jasmin,
On 13/02/14 13:47, Jasmin Blanchette wrote:
Hi Andreas,
Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler
<[email protected]>:
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?
I read the comment to your changeset 3def821deb70, which says that Nat.pred may show up in
theorems generated by primcorec. This is fine, because the destructor view for codatatypes
goes well with discriminators and selectors for datatypes. As I do not know where
discriminators show up in theorems generated by datatype_new, but my guess is that they
only show up in theorems that the old datatype package does not generate. Moreover, I
expect that they do not show up in anyhing generated by primrec. So where would it harm to
make them the official discriminators?
Andreas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
