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

2017-01-23 Thread Andreas Lochbihler
Hi Florian, On 21/01/17 16:56, Florian Haftmann wrote: unfortunately, a selector-based solution didn't either yield a terminating example. If you like you can inspect the attached code, maybe I did get something wrong. I am afraid, I am busy with other stuff and won't have the time to dig into

Re: [isabelle-dev] A note on composition in src/Pure/library.ML

2017-01-23 Thread Lawrence Paulson
I’m not sure what to conclude from this. It’s about non-functional behaviour, so not quite something people ought to rely upon. I’m guessing one could make the change and nothing would happen. I’m still not convinced that the case for a change has been made however. For what it’s worth, there a

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

2017-01-23 Thread Florian Haftmann
Hi Andreas, that should be fine. I am optimistic that we will manage somehow to work that our during February. Cheers, Florian Am 23.01.2017 um 09:39 schrieb Andreas Lochbihler: > Hi Florian, > > On 21/01/17 16:56, Florian Haftmann wrote: >> unfortunately, a selector-based solution did