Email Gateway (Aug 22 2022 at 17:43): Email Gateway (Aug 22 2022 at 17:43):From: Makarius <makarius@sketis.net>
This thread appears to be still open and unanswered. I've briefly tried
it with Isabelle2018-RC2 and Isabelle2017, which produces the same
result. So it is not a regression and not relevant for the Isabelle2018
release process.
Makarius
Email Gateway (Aug 22 2022 at 17:45):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
I had a similar experience with nitpick giving me an obviously wrong
counterexample
for a provable lemma, and it was because I hadn't defined my types
properly-
I don"t know if this applies to your case though.
Best,
Angeliki
Email Gateway (Aug 22 2022 at 17:52):From: Peter Lammich <lammich@in.tum.de>
Hi,
what is happening in the following case, where nitpick reports an
obviously wrong counterexample for a provable lemma, without
indicating that the counterexample might be spurious?
Last updated: Apr 25 2024 at 08:20 UTC