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

2017-04-14 Thread Florian Haftmann
For the record: Lukas and me have resolved that issue in 721feefce9c6. Cheers, Florian Am 14.01.2017 um 09:33 schrieb Florian Haftmann: > Hi Lukas, > > I am currently stuck with a problem in Quickcheck/Narrowing. > > After about 10 years it came to surface that code generation for

Re: [isabelle-dev] Code generation: privacy of exported types in signatures

2017-04-14 Thread Florian Haftmann
Dear Frédéric, I cannot follow reproduce observation; using the attached theory in Isabelle2016-1, I get > structure Foo : sig > type 'a b > type 'a c > val foo : 'a b -> 'a b > end = struct > > datatype 'a a = A; > > datatype 'a b = B of 'a c a > and 'a c = C of 'a b; > > fun foo x =