Re: [isabelle] new quick check expriment

This works:


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


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.