Re: [isabelle] Problems with nitpick



Hi René,

Am 16.10.2014 um 14:21 schrieb René Thiemann <rene.thiemann at uibk.ac.at>:

> I just wanted to report a small problem with nitpick:
> 
> lemma "{1, 2} ⊂ - {7,4 :: int}" 
> Nitpick found a counterexample:
> [...]
> There was no weakening indicating like "possibly spurious counter-example",
> so I was surprised by these wrong counter-examples, since actually
> both statements are provable.

Thank you for your bug report. Generally, there was a bug in the handling of the subset operation in the presence of infinite (or otherwise approximated) types. I have fixed the bug and tested the change locally, and will push it (the change) at the next opportunity.

Regards,

Jasmin





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