Re: [isabelle] Quickcheck counter example of "3 < 4"?



You could do this to get a 'counterexample' in this case:

lemma "set [(1::nat)] â set [2]"
apply rule
quickcheck

Then it works on "!!x. x \in set [1] ==> x \in set [2]" and finds the
counterexample "x = 1".

-Andrew

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 [2]"
>>       quickcheck
>
>>>>> The fact that you are not shown the model is because only the
>>>>> interpretation of the free variables is shown, but there are none.
>>>>>
>>>>> Tobias
>
>   -- Lars
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.