Re: [isabelle] Quickcheck in locale with defines directive



Hi all,

>> locale test =
>>  fixes foo :: "nat"
>>  defines "foo == 0"
>> begin
>>
>>  lemma "foo = 0" unfolding foo_def by rule
>>
>> end

>> Auto Quickcheck found a counterexample:

> Florian, your change d9549f9da779 introduced the above code. Do you know what could be done to take "defines" into consideration?

Well, the change above made quickcheck operate on the interpretations of
a locale rather than just pulling the locale's context into its search
space.  It seems to me that nowadays there are configuration options
»expand« and »interpret« to choose either the naked context or all
interpretations of that particular locale respectively.  Have you tried
the option »expand«?  Maybe there is some documentation on quickcheck
which gives further hints.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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