Re: [isabelle] Problems with nitpick



Hi Rene,

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:
> 
>  Empty assignment
> 
> 
> lemma "{1, 2} ⊂ - {7,4 :: int} ∪ {x}" 
> Nitpick found a counterexample:
> 
>  Free variable:
>    x = 1
> 
> 
> 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.

Thanks for this report. I will look into it, but probably not in the coming three weeks or so unfortunately.

Cheers,

Jasmin





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