Hi Florian, I have been quite busy the last few days and hence did find the time to answer you email quickly.
> This however breaks Quickcheck/Narrowing where the lazy nature of > pattern bindings has been exploited, may be unconsciously. A minimal > example is attached (Quickcheck_Narrowing_Examples.thy) but I also > distilled the generated Haskell code: Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have a evaluation engine that implements narrowing without actually transforming the program that is evaluated. The real ideas how to implement narrowing in Haskell come from the original authors of LazySmallCheck; the main contribution to make this possible in Isabelle is largely the engineering question how to combine the ideas from LazySmallCheck with the Isabelle code generator. As I was investigating this, I did some further extensions to allow existential quantifiers, but this is technically not that difficult to implement. There is a bit of documentation describing the implementation in my thesis. At the moment, I am a little bit busy, but hopefully mid of February, I could assist looking into this. Maintaining Quickcheck Narrowing has not been a major tasks in the last years there was no need to change anything as tricky as the point that we encounter now. Hence, I would expect that maintenance will continue to be low, once we resolved this issue. Lukas _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev