Re: [isabelle] new quick check expriment
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and