[isabelle-dev] Comment in Efficient_Nat

[Lukas Bulwahn]

On 07/22/2012 10:29 AM, Florian Haftmann wrote:
>> text {*
>>    FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
>>    @{text "code_module"} is very aggressive leading to bad Haskell code.
>>    Therefore, we simply deactivate the narrowing-based quickcheck from here on.
>> *}
> I do not unserstand this.  What does "code_module" mean here?  And why
> is it aggressive?
I do recall not the exact details anymore. But I believe that the setup 
with "code_modulename" caused the narrowing-based quickcheck to produce 
non-executable code.
(If I remember correctly, it produced one file with multiple modules, 
which is not valid Haskell code. code_modulename was just to aggressive.)

If you are looking into this and would fix it, that would be great. We 
can discuss the details offline.

Probably related, with the changeset 6efff142bb54, the narrowing-based 
quickcheck fails to generate valid code.

Lukas