[isabelle] new quick check expriment



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
-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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