Re: [isabelle] new quick check expriment
Thanks. It asks me to set 'Environment variable ISABELLE_GHC '. So I uncomment the line 'ISABELLE_GHC="/usr/local/ghc/$ISABELLE_PLATFORM/ghc'
Now it gives me another error message "Compilation with GHC failed". Any suggestion ?
PS, I work in a mac version of Isabelle 2012
On 17 Jun 2012, at 09:23, Tobias Nipkow wrote:
> 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.
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