Re: [isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?



Am 02.09.2014 um 08:01 schrieb Dmitriy Traytel <traytel at in.tum.de>:

> No, I don't know one. At first I thought that in the latter case "BarC_get Bar = BarC_get (BarC None)" would not be provable, but Sledgehammer helped me out: by (metis BarC_get.elims fooD.distinct(1) fooD.inject option.distinct(1)).
> 
> However, Nitpick also reported a non-spurious counterexample (empty assignment), so I'm cc'ing Jasmin.

The answer is given in the first bullet point of Section 8 ("Known Bugs and Limitations") of the Nitpick manual.

Jasmin





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