[isabelle] Quickcheck in locale with defines directive
Consider the following locale:
locale test =
fixes foo :: "nat"
defines "foo == 0"
lemma "foo = 0" unfolding foo_def by rule
Isabelle2014 then produces this output at the lemma statement:
Auto Quickcheck found a counterexample:
foo = Suc 0
0 = 0
So it looks like quickcheck thinks that it can still define "foo",
when it is actually already defined. Or did I misunderstand what the
defines directive does?
This archive was generated by a fusion of
Pipermail (Mailman edition) and