Re: [isabelle] Quickcheck counter example of "3 < 4"?
You could do this to get a 'counterexample' in this case:
lemma "set [(1::nat)] â set "
Then it works on "!!x. x \in set  ==> x \in set " and finds the
counterexample "x = 1".
On Thu, Jul 2, 2015 at 7:17 AM, Lars Noschinski <noschinl at in.tum.de> wrote:
> On 02.07.2015 14:09, Matthew Fernandez wrote:
>> While we're on the topic of quickcheck, why does it fail to show a
>> counterexample for this?
>> lemma "set [(1::nat)] â set "
>>>>> The fact that you are not shown the model is because only the
>>>>> interpretation of the free variables is shown, but there are none.
> -- Lars
This archive was generated by a fusion of
Pipermail (Mailman edition) and