Re: [isabelle] Nitpick falsely produces genuine counterexample
> theory Scratch imports "$AFP/Coinductive/Coinductive" begin
> lemma "ltake â xs = xs"
> nitpick [expect = none]
> by (rule ltake_all) simp
> 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and