Email Gateway (Aug 22 2022 at 19:25): Email Gateway (Aug 22 2022 at 19:25):From: Rei Kristo <reikristo@gmail.com>
Hello,
if
domain B = b | c
lemma "forall a. a = b"
nitpick
quickcheck
then one would expect a counterexample "a := c".
How can I make nitpick and quickcheck find it?
Thank you!
Email Gateway (Aug 22 2022 at 19:25):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Rei,
I’m not sure where the actual problem is:
theory Test
imports Main
begin
datatype B = b | c
lemma "∀ a. a = b”
nitpick (* reports counterexample *)
quickcheck (* reports counterexample *)
end
Best,
René
signature.asc
Email Gateway (Aug 22 2022 at 19:34):From: Rei Kristo <reikristo@gmail.com>
Dear Rene, thank you for the answer.
"Datatype" as Keyword works.
The question is, how do we get quickcheck and nitpick to work with the
Domain-Keyword of HOLCF.
Email Gateway (Aug 22 2022 at 19:35):From: Rei Kristo <reikristo@gmail.com>
I see.
Perhaps You or Mr.Blanchette could help me by recommending / forwarding the
question to someone?
It would also be interesting to learn more about the following related but
unanswered old question of John Matthews:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2005-September/msg00016.html
Thank You!
Last updated: Apr 24 2024 at 08:20 UTC