Email Gateway (Aug 19 2022 at 16:19): Email Gateway (Aug 19 2022 at 16:19):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
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.
Kind regards,
René
Email Gateway (Aug 19 2022 at 16:20):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Rene,
Thanks for this report. I will look into it, but probably not in the coming three weeks or so unfortunately.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 16:27):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi René,
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
Last updated: Nov 21 2024 at 12:39 UTC