[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers

2008-06-20 Thread Benedikt Huber
Levi Stephen schrieb: On Fri, Jun 20, 2008 at 3:30 AM, Benedikt Huber [EMAIL PROTECTED] wrote: Levi Stephen schrieb: Hi, I have the following definitions type Zero type Succ a so that I can muck around with a Vector type that includes its length encoded in its type. I was wondering whether

[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers

2008-06-19 Thread Benedikt Huber
Levi Stephen schrieb: Hi, I have the following definitions type Zero type Succ a so that I can muck around with a Vector type that includes its length encoded in its type. I was wondering whether it was possible to use SmallCheck (or QuickCheck) to generate random Peano numbers? Is there an

[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers

2008-06-19 Thread Levi Stephen
If so, you could write a SmallCheck Series instance as follows. instance Serial (Vec Zero a) where series = cons0 nil instance (Serial a, Serial (Vec n a)) = Serial (Vec (Succ n) a) where series = cons2 (|) If we have the property prop_vector :: Vec (Succ (Succ Zero)) Bool -

[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers

2008-06-19 Thread Levi Stephen
On Fri, Jun 20, 2008 at 3:30 AM, Benedikt Huber [EMAIL PROTECTED] wrote: Levi Stephen schrieb: Hi, I have the following definitions type Zero type Succ a so that I can muck around with a Vector type that includes its length encoded in its type. I was wondering whether it was possible