Re: [isabelle] Nitpick falsely produces genuine counterexample



Dear Denis,

> theory Scratch imports "$AFP/Coinductive/Coinductive" begin
> 
> lemma "ltake â xs = xs"
>  nitpick [expect = none]
>  by (rule ltake_all) simp
> 
> end
> 
> I'm not sure if this case is covered by Section 8 "Known Bugs and
> Limitations" in the Nitpick Userguide, so I decided to post the example
> anyway.

Thanks for posting it! It is indeed a genuine counterexample to the soundness of Nitpick. I will look into it.

Appeal to the mailing list: Nitpick is not supposed to produce spurious counterexamples (except when it warns you about a âpotentially spuriousâ counterexample in its message already). If you run into cases like the one reported by Denis, this is not normal and I would love to have a reproducible example.

Jasmin





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