Re: [isabelle] new quick check expriment



This works:

quickcheck[narrowing]

Admittedly, it would be nice if that option were not necessary.

Tobias

Am 17/06/2012 02:20, schrieb Yuhui Lin:
> HI all,
> 
> I'm playing the Isabelle 2012 to test the enhanced quickcheck. According to the paper "The New Quickcheck for Isabelle", quick check should be able to find a counter example for the lemma "xs = rev xs ==> EX ys. xs = ys @ rev ys". I failed to get this result, but an error message complaining about 
> 
> "*** Wellsortedness error:
> *** Type Enum.finite_1 list not of sort enum
> *** No type arity list :: enum
> 
> Do I miss any config to enable the narrowing-based testing ? How can I get the counter example with narrowing-based testing? Thanks.
> 
> Best,
> Yuhui





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