[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 whethe

[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 wonderin

[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)

[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 i