{-# language DeriveGeneric #-}
module Blueprint where

import Test.LeanCheck
import Test.LeanCheck.Generic
import GHC.Generics

data Nat = Z | S Nat
     deriving (Eq, Show, Generic)

instance Listable Nat where tiers = genericTiers

plus :: Nat -> Nat -> Nat
plus x y = case x of
     Z -> y
     S x'  -> S ( plus x' y )

double :: Nat -> Nat
double x = case x of
       Z -> Z
       S x' -> S ( S ( double x' ) )

t1 =  S (S Z ) 

test :: Bool
test = and
         [ double ( S (S Z ) ) == S ( S ( S ( S Z ) ) ) 
         , holds 1000 $ \ x ->
                double (x :: Nat) == plus x x
         ]