Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

Hi Andreas, thanks for that quick reply. This could be done in any case, sure. Cheers, Florian Am 14.01.2017 um 10:03 schrieb Andreas Lochbihler: > Hi Florian, > > Lukas may be able to answer this question better, but here's a comment: > You do not need the lazy treatment of

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

Hi Florian, Lukas may be able to answer this question better, but here's a comment: You do not need the lazy treatment of irrefutable patterns in Haskell as a primitive, because it is easy to emulate using selectors. That is, if we have a single-constructor HOL datatype dataype 'a T = C (s1:

[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

Hi Lukas, I am currently stuck with a problem in Quickcheck/Narrowing. After about 10 years it came to surface that code generation for Haskell may produce irrefutable patterns due to pattern bindings in let clauses. See ; if I understand