diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,16 +1,28 @@
 LeanCheck
 =========
 
-**The API is likely to change in the near future**
+LeanCheck is a simple enumerative [property-based testing] library.  Properties
+are defined as Haskell functions returning a boolean value which should be
+`True` for all possible choices of argument values.    LeanCheck applies
+enumerated argument values to these properties in search for a counterexample.
+Properties can be viewed as parameterized unit tests.
 
-LeanCheck is a simple enumerative property-based testing library.  It works by
-producing *tiers* of test values, which are essentially (possibly infinite)
-lists of finite lists of same-and-increasingly-sized values.  It is similar to
-[Feat] in that regard.
+LeanCheck works by producing *tiers* of test values: a possibly infinite list
+of finite sublists of same-and-increasingly-sized values.  This enumeration is
+similar to [Feat]'s.  However, the ranking and ordering of values are defined
+differently.  The interface is also different.
 
 In this README, lines ending with `-- >` indicate expected return values.
 
 
+Installing
+----------
+
+To install the latest LeanCheck version from Hackage, just run:
+
+	$ cabal install leancheck
+
+
 Checking if properties are True
 -------------------------------
 
@@ -22,7 +34,7 @@
 then, it returns a boolean indicating whether the property holds.
 See (ghci):
 
-	import Test.Check
+	import Test.LeanCheck
 	import Data.List
 	holds 100 $ \xs -> sort (sort xs) == sort (xs::[Int])  -- > True
 	holds 100 $ \xs -> [] `union` xs == (xs::[Int])        -- > False
@@ -40,7 +52,7 @@
 representing the offending arguments to the property.
 See (ghci):
 
-	import Test.Check
+	import Test.LeanCheck
 	import Data.List
 
 	counterExample 100 $ \xs -> sort (sort xs) == sort (xs::[Int])
@@ -60,14 +72,14 @@
 automatically printing results on standard output,
 you can use the function `check :: Testable a => a -> IO ()`.
 
-	import Test.Check
+	import Test.LeanCheck
 	import Data.List
 
 	check $ \xs -> sort (sort xs) == sort (xs::[Int])
-	-- > OK, passed 200 tests.
+	-- > +++ OK, passed 200 tests.
 
 	check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
-	-- > Failed! Falsifiable (after 4 tests):
+	-- > *** Failed! Falsifiable (after 4 tests):
 	-- > [] [0,0]
 
 The function `check` tests for a maximum of 200 tests.
@@ -76,11 +88,11 @@
 There is no "quiet" option, just use `holds` or `counterExample` in that case.
 
 
-Testing for custom types
-------------------------
+Testing user-defined types
+--------------------------
 
-LeanCheck works on properties with `Listable` argument types.
-Custom `Listable` instances are created similarly to SmallCheck:
+LeanCheck works on properties with [`Listable`] argument types.
+`Listable` instances are declared similarly to SmallCheck:
 
 	data MyType = MyConsA
 	            | MyConsB Int
@@ -93,13 +105,13 @@
 	       \/ cons2 MyConsC
 	       \/ cons1 MyConsD
 
-The tiers function return a potentially infinite list of finite sub-lists (tiers).
-Each tier has values of increasing size.
+The `tiers` function return a potentially infinite list of finite sub-lists
+(tiers).  Each successive tier has values of increasing size.
 
 	tiers :: Listable a => [[a]]
 
-For convenience, there is also the function `list`,
-which returns an infinite list of values of the bound type:
+For convenience, the function `list` returns a potentially infinite list
+of values of the bound type:
 
 	list :: Listable a => [a]
 
@@ -109,42 +121,26 @@
 
 The `list` function can be used to debug your custom instances.
 
-
-More information / extra functions
-----------------------------------
-
-`Listable` class instances are more customizable than what is described here:
+[`Listable`] class instances are more customizable than what is described here:
 check source comments or haddock documentation for details.
 
 
-Building / Installing
----------------------
-
-To build:
-
-	$ cabal build
-
-To install:
-
-	$ cabal install
-
-To reference in a cabal sandbox:
-
-	$ cabal sandbox add-source ../path/to/leancheck
-
-To use the files directly in your project:
-
-	$ cp -r Test ../path/to/your-project
+Further reading
+---------------
 
+For a detailed documentation of each function, see
+[LeanCheck's Haddock documentation].
 
-LeanCheck was tested on GHC 7.10, GHC 7.8, GHC 7.6 and GHC 7.4.
-This library does not use any fancy extensions:
-if it does not work on previous GHC versions,
-probably only *minor* changes are needed.
-It optionally depends on Template Haskell
-(for automatic derivation of Listable instances).
+For an introduction to property-based testing
+and a step-by-step guide to LeanCheck, see this
+[tutorial on property-based testing with LeanCheck].
 
+[LeanCheck's Haddock documentation]: https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html
+[tutorial on property-based testing with LeanCheck]: doc/tutorial.md
+[`Listable`]: https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#t:Listable
 
+[property-based testing]: doc/tutorial.md
 [Feat]: https://hackage.haskell.org/package/testing-feat
 [SmallCheck]: https://hackage.haskell.org/package/smallcheck
 [QuickCheck]: https://hackage.haskell.org/package/QuickCheck
+
diff --git a/Test/Check.hs b/Test/Check.hs
deleted file mode 100644
--- a/Test/Check.hs
+++ /dev/null
@@ -1,112 +0,0 @@
--- | A simple property-based testing library based on
---   enumeration of values via lists of lists.
---
--- In the context of this library,
--- a __property__ is a function returning a 'Bool'
--- that should return 'True' for all input values.
---
--- To check if a property holds by testing a thousand values, you simply do:
---
--- > holds 1000 property  -- yield True when Ok, False otherwise
---
--- For example:
---
--- > holds $ \xs -> length (sort xs) == length (xs::[Int])
---
--- Arguments of properties should be instances of the 'Listable' typeclass.
--- 'Listable' instances are provided for the most common Haskell types.
--- New instances are easily defined
--- (see the 'Listable's documentation for more info).
-module Test.Check
-  (
-  -- * Checking and testing
-    holds
-  , fails
-  , exists
-
-  -- ** Boolean (property) operators
-  , (==>)
-
-  -- ** Counterexamples and witnesses
-  , counterExample
-  , counterExamples
-  , witness
-  , witnesses
-
-  -- * Listing test values
-  , Listable(..)
-
-  -- ** Listing constructors
-  , cons0
-  , cons1
-  , cons2
-  , cons3
-  , cons4
-  , cons5
-  , cons6
-  , cons7
-  , cons8
-  , cons9
-  , cons10
-  , cons11
-  , cons12
-
-  , ofWeight
-  , addWeight
-  , suchThat
-
-  -- ** Combining tiers
-  , (\/)
-  , (\\//)
-  , (><)
-  , productWith
-
-  -- ** Manipulating tiers
-  , mapT
-  , filterT
-  , concatT
-  , concatMapT
-  , deleteT
-  , normalizeT
-  , toTiers
-
-  -- ** Automatically deriving Listable instances
-  , deriveListable
-
-  -- ** Extra constructors
-  , consFromList
-  , consFromAscendingList
-  , consFromStrictlyAscendingList
-  , consFromSet
-  , consFromNoDupList
-
-  -- ** Products of tiers
-  , product3With
-  , productMaybeWith
-
-  -- * Listing lists
-  , listsOf
-  , setsOf
-  , ascendingListsOf
-  , strictlyAscendingListsOf
-  , noDupListsOf
-  , products
-  , listsOfLength
-
-  -- ** Listing values
-  , tiersFractional
-  , listIntegral
-  , (+|)
-
-  -- * Test results
-  , Testable
-  , results
-
-  , module Test.Check.IO
-  )
-where
-
-import Test.Check.Basic
-import Test.Check.Utils
-import Test.Check.Derive
-import Test.Check.IO
diff --git a/Test/Check/Basic.hs b/Test/Check/Basic.hs
deleted file mode 100644
--- a/Test/Check/Basic.hs
+++ /dev/null
@@ -1,123 +0,0 @@
--- | Simple property-based testing library based on
---   enumeration of values via lists of lists.
---
--- This module exports "Test.Check.Core" functionality along with instances and
--- functions for further tuple and constructor arities.
---
--- For the complete list of functions, see "Test.Check".
-module Test.Check.Basic
-  ( module Test.Check.Core
-
-  , cons6
-  , cons7
-  , cons8
-  , cons9
-  , cons10
-  , cons11
-  , cons12
-  )
-where
-
-import Test.Check.Core
-
-instance (Listable a, Listable b, Listable c,
-          Listable d, Listable e, Listable f) =>
-         Listable (a,b,c,d,e,f) where
-  tiers = productWith (\x (y,z,w,v,u) -> (x,y,z,w,v,u)) tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d,
-          Listable e, Listable f, Listable g) =>
-         Listable (a,b,c,d,e,f,g) where
-  tiers = productWith (\x (y,z,w,v,u,r) -> (x,y,z,w,v,u,r)) tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d,
-          Listable e, Listable f, Listable g, Listable h) =>
-         Listable (a,b,c,d,e,f,g,h) where
-  tiers = productWith (\x (y,z,w,v,u,r,s) -> (x,y,z,w,v,u,r,s))
-                      tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d, Listable e,
-          Listable f, Listable g, Listable h, Listable i) =>
-         Listable (a,b,c,d,e,f,g,h,i) where
-  tiers = productWith (\x (y,z,w,v,u,r,s,t) -> (x,y,z,w,v,u,r,s,t))
-                      tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d, Listable e,
-          Listable f, Listable g, Listable h, Listable i, Listable j) =>
-         Listable (a,b,c,d,e,f,g,h,i,j) where
-  tiers = productWith (\x (y,z,w,v,u,r,s,t,o) -> (x,y,z,w,v,u,r,s,t,o))
-                      tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d,
-          Listable e, Listable f, Listable g, Listable h,
-          Listable i, Listable j, Listable k) =>
-         Listable (a,b,c,d,e,f,g,h,i,j,k) where
-  tiers = productWith (\x (y,z,w,v,u,r,s,t,o,p) -> (x,y,z,w,v,u,r,s,t,o,p))
-                      tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d,
-          Listable e, Listable f, Listable g, Listable h,
-          Listable i, Listable j, Listable k, Listable l) =>
-         Listable (a,b,c,d,e,f,g,h,i,j,k,l) where
-  tiers = productWith (\x (y,z,w,v,u,r,s,t,o,p,q) ->
-                        (x,y,z,w,v,u,r,s,t,o,p,q))
-                      tiers tiers
-
-cons6 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f)
-      => (a -> b -> c -> d -> e -> f -> g) -> [[g]]
-cons6 f = mapT (uncurry6 f) tiers `addWeight` 1
-
-cons7 :: (Listable a, Listable b, Listable c, Listable d,
-          Listable e, Listable f, Listable g)
-      => (a -> b -> c -> d -> e -> f -> g -> h) -> [[h]]
-cons7 f = mapT (uncurry7 f) tiers `addWeight` 1
-
-cons8 :: (Listable a, Listable b, Listable c, Listable d,
-          Listable e, Listable f, Listable g, Listable h)
-      => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> [[i]]
-cons8 f = mapT (uncurry8 f) tiers `addWeight` 1
-
-cons9 :: (Listable a, Listable b, Listable c, Listable d, Listable e,
-          Listable f, Listable g, Listable h, Listable i)
-      => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> [[j]]
-cons9 f = mapT (uncurry9 f) tiers `addWeight` 1
-
-cons10 :: (Listable a, Listable b, Listable c, Listable d, Listable e,
-           Listable f, Listable g, Listable h, Listable i, Listable j)
-       => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> [[k]]
-cons10 f = mapT (uncurry10 f) tiers `addWeight` 1
-
-cons11 :: (Listable a, Listable b, Listable c, Listable d,
-           Listable e, Listable f, Listable g, Listable h,
-           Listable i, Listable j, Listable k)
-       => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> [[l]]
-cons11 f = mapT (uncurry11 f) tiers `addWeight` 1
-
-cons12 :: (Listable a, Listable b, Listable c, Listable d,
-           Listable e, Listable f, Listable g, Listable h,
-           Listable i, Listable j, Listable k, Listable l)
-       => (a->b->c->d->e->f->g->h->i->j->k->l->m) -> [[m]]
-cons12 f = mapT (uncurry12 f) tiers `addWeight` 1
-
-uncurry6 :: (a->b->c->d->e->f->g) -> (a,b,c,d,e,f) -> g
-uncurry6 f (x,y,z,w,v,u) = f x y z w v u
-
-uncurry7 :: (a->b->c->d->e->f->g->h) -> (a,b,c,d,e,f,g) -> h
-uncurry7 f (x,y,z,w,v,u,r) = f x y z w v u r
-
-uncurry8 :: (a->b->c->d->e->f->g->h->i) -> (a,b,c,d,e,f,g,h) -> i
-uncurry8 f (x,y,z,w,v,u,r,s) = f x y z w v u r s
-
-uncurry9 :: (a->b->c->d->e->f->g->h->i->j) -> (a,b,c,d,e,f,g,h,i) -> j
-uncurry9 f (x,y,z,w,v,u,r,s,t) = f x y z w v u r s t
-
-uncurry10 :: (a->b->c->d->e->f->g->h->i->j->k) -> (a,b,c,d,e,f,g,h,i,j) -> k
-uncurry10 f (x,y,z,w,v,u,r,s,t,o) = f x y z w v u r s t o
-
-uncurry11 :: (a->b->c->d->e->f->g->h->i->j->k->l)
-          -> (a,b,c,d,e,f,g,h,i,j,k) -> l
-uncurry11 f (x,y,z,w,v,u,r,s,t,o,p) = f x y z w v u r s t o p
-
-uncurry12 :: (a->b->c->d->e->f->g->h->i->j->k->l->m)
-          -> (a,b,c,d,e,f,g,h,i,j,k,l) -> m
-uncurry12 f (x,y,z,w,v,u,r,s,t,o,p,q) = f x y z w v u r s t o p q
diff --git a/Test/Check/Core.hs b/Test/Check/Core.hs
deleted file mode 100644
--- a/Test/Check/Core.hs
+++ /dev/null
@@ -1,384 +0,0 @@
--- | Simple property-based testing library based on
---   enumeration of values via lists of lists.
---
--- This is the core module of the library, with the most basic definitions.  If
--- you are looking just to use the library, import and see "Test.Check".
---
--- If you want to understand how the code works, this is the place to start.
---
---
--- Other important modules:
---
--- "Test.Check.Basic" re-exports (almost) everything from this module
---         along with constructors and instances for further arities.
---
--- "Test.Check.Utils" re-exports "Test.Check.Basic"
---         along with functions for advanced Listable instance definitions.
---
--- "Test.Check" re-exports "Test.Check.Utils"
---   along with a TH function to automatically derive Listable instances.
-module Test.Check.Core
-  (
-  -- * Checking and testing
-    holds
-  , fails
-  , exists
-  , counterExample
-  , counterExamples
-  , witness
-  , witnesses
-  , Testable
-
-  , results
-
-  -- * Listing test values
-  , Listable(..)
-
-  -- ** Constructing lists of tiers
-  , cons0
-  , cons1
-  , cons2
-  , cons3
-  , cons4
-  , cons5
-
-  , ofWeight
-  , addWeight
-  , suchThat
-
-  -- ** Combining lists of tiers
-  , (\/), (\\//)
-  , (><)
-  , productWith
-
-  -- ** Manipulating lists of tiers
-  , mapT
-  , filterT
-  , concatT
-  , concatMapT
-  , toTiers
-
-  -- ** Boolean (property) operators
-  , (==>)
-
-  -- ** Misc utilities
-  , (+|)
-  , listIntegral
-  , tiersFractional
-  )
-where
-
-import Data.Maybe (listToMaybe)
-
-
--- | A type is 'Listable' when there exists a function that
---   is able to list (ideally all of) its values.
---
--- Ideally, this type should be defined by a 'tiers' function that
--- returns a (possibly infinite) list of finite sub-lists (tiers):
---   the first sub-list contains elements of size 0,
---   the second sub-list contains elements of size 1
---   and so on.
--- Size here is defined by the implementor of the type-class instance.
---
--- For algebraic data types, the general form for 'tiers' is:
---
--- > tiers = consN ConstructorA
--- >      \/ consN ConstructorB
--- >      \/ consN ConstructorC
--- >      \/ ...
---
--- When defined by 'list', each sub-list in 'tiers' is a singleton list
--- (each element of 'list' has +1 size).
---
--- The function 'Test.Check.Derive.deriveListable' from "Test.Check.Derive"
--- can automatically derive instances of this typeclass.
---
--- A 'Listable' instance for functions is also available but is not exported by
--- default.  Import "Test.Check.Function" for that.
--- ("Test.Check.Function.Show" for a Show instance for functions)
-class Listable a where
-  tiers :: [[a]]
-  list :: [a]
-  tiers = toTiers list
-  list = concat tiers
-  {-# MINIMAL list | tiers #-}
-
--- | Takes a list of values @xs@ and transform it into tiers on which each
---   tier is occupied by a single element from @xs@.
---
--- To convert back to a list, just 'concat'.
-toTiers :: [a] -> [[a]]
-toTiers = map (:[])
-
-instance Listable () where
-  list = [()]
-
-listIntegral :: (Enum a, Num a) => [a]
-listIntegral = [0,-1..] +| [1..]
-
-instance Listable Int where
-  list = listIntegral
-
-instance Listable Integer where
-  list = listIntegral
-
-instance Listable Char where
-  list = ['a'..'z']
-      +| [' ','\n']
-      +| ['A'..'Z']
-      +| ['0'..'9']
-      +| ['!'..'/']
-      +| ['\t']
-      +| [':'..'@']
-      +| ['['..'`']
-      +| ['{'..'~']
-
-instance Listable Bool where
-  tiers = cons0 False \/ cons0 True
-
-instance Listable a => Listable (Maybe a) where
-  tiers = cons0 Nothing \/ cons1 Just
-
-instance (Listable a, Listable b) => Listable (Either a b) where
-  tiers = cons1 Left  `ofWeight` 0
-     \\// cons1 Right `ofWeight` 0
-
-instance (Listable a, Listable b) => Listable (a,b) where
-  tiers = tiers >< tiers
-
-instance (Listable a, Listable b, Listable c) => Listable (a,b,c) where
-  tiers = productWith (\x (y,z) -> (x,y,z)) tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d) =>
-         Listable (a,b,c,d) where
-  tiers = productWith (\x (y,z,w) -> (x,y,z,w)) tiers tiers
-
-instance (Listable a, Listable b, Listable c, Listable d, Listable e) =>
-         Listable (a,b,c,d,e) where
-  tiers = productWith (\x (y,z,w,v) -> (x,y,z,w,v)) tiers tiers
-
-instance (Listable a) => Listable [a] where
-  tiers = cons0 []
-       \/ cons2 (:)
-
--- | Tiers of 'Fractional' values.
---   This can be used as the implementation of 'tiers' for 'Fractional' types.
-tiersFractional :: Fractional a => [[a]]
-tiersFractional = productWith (+) tiersFractionalParts
-                                  (mapT fromIntegral (tiers::[[Integer]]))
-               \/ [ [], [], [1/0], [-1/0] {- , [-0], [0/0] -} ]
-  where tiersFractionalParts :: Fractional a => [[a]]
-        tiersFractionalParts = [0]
-                             : [ [fromIntegral a / fromIntegral b]
-                               | b <- iterate (*2) 2, a <- [1::Integer,3..b] ]
--- The position of Infinity in the above enumeration is arbitrary.
-
--- Note that this instance ignores NaN's.
-instance Listable Float where
-  tiers = tiersFractional
-
-instance Listable Double where
-  tiers = tiersFractional
-
-
--- | 'map' over tiers
-mapT :: (a -> b) -> [[a]] -> [[b]]
-mapT = map . map
-
--- | 'filter' tiers
-filterT :: (a -> Bool) -> [[a]] -> [[a]]
-filterT f = map (filter f)
-
--- | 'concat' tiers of tiers
-concatT :: [[ [[a]] ]] -> [[a]]
-concatT = foldr (\+:/) [] . map (foldr (\/) [])
-  where xss \+:/ yss = xss \/ ([]:yss)
-
--- | 'concatMap' over tiers
-concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]]
-concatMapT f = concatT . mapT f
-
-
--- | Takes a constructor with no arguments and return tiers (with a single value).
---   This value, by default, has size/weight 0.
-cons0 :: a -> [[a]]
-cons0 x = [[x]]
-
--- | Takes a constructor with one argument and return tiers of that value.
---   This value, by default, has size/weight 1.
-cons1 :: Listable a => (a -> b) -> [[b]]
-cons1 f = mapT f tiers `addWeight` 1
-
--- | Takes a constructor with two arguments and return tiers of that value.
---   This value, by default, has size/weight 1.
-cons2 :: (Listable a, Listable b) => (a -> b -> c) -> [[c]]
-cons2 f = mapT (uncurry f) tiers `addWeight` 1
-
-cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]]
-cons3 f = mapT (uncurry3 f) tiers `addWeight` 1
-
-cons4 :: (Listable a, Listable b, Listable c, Listable d)
-      => (a -> b -> c -> d -> e) -> [[e]]
-cons4 f = mapT (uncurry4 f) tiers `addWeight` 1
-
-cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e)
-      => (a -> b -> c -> d -> e -> f) -> [[f]]
-cons5 f = mapT (uncurry5 f) tiers `addWeight` 1
-
--- | Resets the weight of a constructor (or tiers)
--- Typically used as an infix constructor when defining Listable instances:
---
--- > cons<N> `ofWeight` W
---
--- Be careful: do not apply @`ofWeight` 0@ to recursive data structure
--- constructors.  In general this will make the list of size 0 infinite,
--- breaking the tier invariant (each tier must be finite).
-ofWeight :: [[a]] -> Int -> [[a]]
-ofWeight xss w = dropWhile null xss `addWeight` w
-
--- | Adds to the weight of tiers of a constructor
-addWeight :: [[a]] -> Int -> [[a]]
-addWeight xss w = replicate w [] ++ xss
-
--- | Tiers of values that follow a property
---
--- > cons<N> `suchThat` condition
-suchThat :: [[a]] -> (a->Bool) -> [[a]]
-suchThat = flip filterT
-
--- | Lazily interleaves two lists, switching between elements of the two.
---   Union/sum of the elements in the lists.
---
--- > [x,y,z] +| [a,b,c] == [x,a,y,b,z,c]
-(+|) :: [a] -> [a] -> [a]
-[]     +| ys = ys
-(x:xs) +| ys = x:(ys +| xs)
-infixr 5 +|
-
--- | Append tiers.
---
--- > [xs,ys,zs,...] \/ [as,bs,cs,...] = [xs++as,ys++bs,zs++cs,...]
-(\/) :: [[a]] -> [[a]] -> [[a]]
-xss \/ []  = xss
-[]  \/ yss = yss
-(xs:xss) \/ (ys:yss) = (xs ++ ys) : xss \/ yss
-infixr 7 \/
-
--- | Interleave tiers.  When in doubt, use @\/@ instead.
---
--- > [xs,ys,zs,...] \/ [as,bs,cs,...] = [xs+|as,ys+|bs,zs+|cs,...]
-(\\//) :: [[a]] -> [[a]] -> [[a]]
-xss \\// []  = xss
-[]  \\// yss = yss
-(xs:xss) \\// (ys:yss) = (xs +| ys) : xss \\// yss
-infixr 7 \\//
-
--- | Take a tiered product of lists of tiers.
---
--- > [t0,t1,t2,...] >< [u0,u1,u2,...] =
--- > [ t0**u0
--- > , t0**u1 ++ t1**u0
--- > , t0**u2 ++ t1**u1 ++ t2**u0
--- > , ...       ...       ...       ...
--- > where xs ** ys = [(x,y) | x <- xs, y <- ys]
---
--- Example:
---
--- > [[0],[1],[2],...] >< [[0],[1],[2],...]
--- > == [  [(0,0)]
--- >    ,  [(1,0),(0,1)]
--- >    ,  [(2,0),(1,1),(0,2)]
--- >    ,  [(3,0),(2,1),(1,2),(0,3)]
--- >    ...
--- >    ]
-(><) :: [[a]] -> [[b]] -> [[(a,b)]]
-(><) = productWith (,)
-infixr 8 ><
-
--- | Take the product of two lists of tiers.
---
--- > productWith f xss yss = map (uncurry f) $ xss >< yss
-productWith :: (a->b->c) -> [[a]] -> [[b]] -> [[c]]
-productWith _ _ [] = []
-productWith _ [] _ = []
-productWith f (xs:xss) yss = map (xs **) yss
-                          \/ productWith f xss yss `addWeight` 1
-  where xs ** ys = [x `f` y | x <- xs, y <- ys]
-
--- | 'Testable' values are functions
---   of 'Listable' arguments that return boolean values,
---   e.g.:
---
--- * @ Bool @
--- * @ Int -> Bool @
--- * @ Listable a => a -> a -> Bool @
-class Testable a where
-  resultiers :: a -> [[([String],Bool)]]
-
-instance Testable Bool where
-  resultiers p = [[([],p)]]
-
-instance (Testable b, Show a, Listable a) => Testable (a->b) where
-  resultiers p = concatMapT resultiersFor tiers
-    where resultiersFor x = mapFst (showsPrec 11 x "":) `mapT` resultiers (p x)
-          mapFst f (x,y) = (f x, y)
-
--- | List all results of a 'Testable' property.
--- Each results is composed by a list of strings and a boolean.
--- The list of strings represents the arguments applied to the function.
--- The boolean tells whether the property holds for that selection of argument.
--- This list is usually infinite.
-results :: Testable a => a -> [([String],Bool)]
-results = concat . resultiers
-
--- | Lists all counter-examples for a number of tests to a property,
-counterExamples :: Testable a => Int -> a -> [[String]]
-counterExamples n = map fst . filter (not . snd) . take n . results
-
--- | For a number of tests to a property,
---   returns Just the first counter-example or Nothing.
-counterExample :: Testable a => Int -> a -> Maybe [String]
-counterExample n = listToMaybe . counterExamples n
-
--- | Lists all witnesses for a number of tests to a property,
-witnesses :: Testable a => Int -> a -> [[String]]
-witnesses n = map fst . filter snd . take n . results
-
--- | For a number of tests to a property,
---   returns Just the first witness or Nothing.
-witness :: Testable a => Int -> a -> Maybe [String]
-witness n = listToMaybe . witnesses n
-
--- | Does a property __hold__ for a number of test values?
---
--- > holds 1000 $ \xs -> length (sort xs) == length xs
-holds :: Testable a => Int -> a -> Bool
-holds n = and . take n . map snd . results
-
--- | Does a property __fail__ for a number of test values?
---
--- > fails 1000 $ \xs -> xs ++ ys == ys ++ xs
-fails :: Testable a => Int -> a -> Bool
-fails n = not . holds n
-
--- | There __exists__ and assignment of values that satisfy a property?
-exists :: Testable a => Int -> a -> Bool
-exists n = or . take n . map snd . results
-
-uncurry3 :: (a->b->c->d) -> (a,b,c) -> d
-uncurry3 f (x,y,z) = f x y z
-
-uncurry4 :: (a->b->c->d->e) -> (a,b,c,d) -> e
-uncurry4 f (x,y,z,w) = f x y z w
-
-uncurry5 :: (a->b->c->d->e->f) -> (a,b,c,d,e) -> f
-uncurry5 f (x,y,z,w,v) = f x y z w v
-
--- | Boolean implication.  Use this for defining conditional properties:
---
--- > prop_something x y = condition x y ==> something x y
-(==>) :: Bool -> Bool -> Bool
-False ==> _ = True
-True  ==> p = p
-infixr 0 ==>
diff --git a/Test/Check/Derive.hs b/Test/Check/Derive.hs
deleted file mode 100644
--- a/Test/Check/Derive.hs
+++ /dev/null
@@ -1,153 +0,0 @@
-{-# LANGUAGE TemplateHaskell, CPP #-}
--- Experimental module for deriving Listable instances
---
--- Needs GHC and Template Haskell (tested on GHC 7.4, 7.6, 7.8 and 7.10)
-module Test.Check.Derive
-  ( deriveListable
-  )
-where
-
-import Language.Haskell.TH
-import Test.Check.Basic
-import Control.Monad (unless, liftM, liftM2)
-
-#if __GLASGOW_HASKELL__ < 706
--- reportWarning was only introduced in GHC 7.6 / TH 2.8
-reportWarning :: String -> Q ()
-reportWarning = report False
-#endif
-
--- | Derives a Listable instance for a given type ('Name').
-deriveListable :: Name -> DecsQ
-deriveListable t = do
-  is <- t `isInstanceOf` ''Listable
-  if is
-    then do reportWarning $ "Instance Listable "
-                         ++ show t
-                         ++ " already exists, skipping derivation"
-            return []
-    else do cd <- canDeriveListable t
-            unless cd (fail $ "Unable to derive Listable "
-                           ++ show t)
-            reallyDeriveListable t
-
--- | Checks whether it is possible to derive a Listable instance.
---
--- For example, it is not possible if there are is no Listable instance for a
--- type in one of the constructors.
-canDeriveListable :: Name -> Q Bool
-canDeriveListable t = return True -- TODO: Check instances for type-cons args
-
--- TODO: Somehow check if the enumeration has repetitions, then warn the user.
-reallyDeriveListable :: Name -> DecsQ
-reallyDeriveListable t = do
-  (nt,vs) <- normalizeType t
-#if __GLASGOW_HASKELL__ >= 710
-  cxt <- sequence [[t| Listable $(return v) |] | v <- vs]
-#else
-  cxt <- sequence [classP ''Listable [return v] | v <- vs]
-#endif
-#if __GLASGOW_HASKELL__ >= 708
-  cxt |=>| [d| instance Listable $(return nt)
-                 where tiers = $(conse =<< typeCons t) |]
-#else
-  tiersE <- conse =<< typeCons t
-  return [ InstanceD
-             cxt
-             (AppT (ConT ''Listable) nt)
-             [ValD (VarP 'tiers) (NormalB tiersE) []]
-         ]
-#endif
-  where cone n arity = do
-          (Just consN) <- lookupValueName $ "cons" ++ show arity
-          [| $(varE consN) $(conE n) |]
-        conse = foldr1 (\e1 e2 -> [| $e1 \/ $e2 |]) . map (uncurry cone)
-
-
--- * Template haskell utilities
-
--- Normalizes a type by applying it to necessary type variables, making it
--- accept "zero" parameters.  The normalized type is tupled with a list of
--- necessary type variables.
---
--- Suppose:
---
--- > data DT a b c ... = ...
---
--- Then, in pseudo-TH:
---
--- > normalizeType [t|DT|] == Q (DT a b c ..., [a, b, c, ...])
-normalizeType :: Name -> Q (Type, [Type])
-normalizeType t = do
-  ar <- typeArity t
-  vs <- newVarTs ar
-  return (foldl AppT (ConT t) vs, vs)
-  where
-    newNames :: [String] -> Q [Name]
-    newNames = mapM newName
-    newVarTs :: Int -> Q [Type]
-    newVarTs n = liftM (map VarT)
-               $ newNames (take n . map (:[]) $ cycle ['a'..'z'])
-
--- Normalizes a type by applying it to units (`()`) while possible.
---
--- > normalizeTypeUnits ''Int    === [t| Int |]
--- > normalizeTypeUnits ''Maybe  === [t| Maybe () |]
--- > normalizeTypeUnits ''Either === [t| Either () () |]
-normalizeTypeUnits :: Name -> Q Type
-normalizeTypeUnits t = do
-  ar <- typeArity t
-  return (foldl AppT (ConT t) (replicate ar (TupleT 0)))
-
--- Given a type name and a class name,
--- returns whether the type is an instance of that class.
-isInstanceOf :: Name -> Name -> Q Bool
-isInstanceOf tn cl = do
-  ty <- normalizeTypeUnits tn
-  isInstance cl [ty]
-
--- | Given a type name, return the number of arguments taken by that type.
--- Examples in partially broken TH:
---
--- > arity ''Int        === Q 0
--- > arity ''Int->Int   === Q 0
--- > arity ''Maybe      === Q 1
--- > arity ''Either     === Q 2
--- > arity ''Int->      === Q 1
---
--- This works for Data's and Newtype's and it is useful when generating
--- typeclass instances.
-typeArity :: Name -> Q Int
-typeArity t = do
-  ti <- reify t
-  return . length $ case ti of
-    TyConI (DataD    _ _ ks _ _) -> ks
-    TyConI (NewtypeD _ _ ks _ _) -> ks
-    _                            -> error $ "error (arity): symbol "
-                                         ++ show t
-                                         ++ " is not a newtype or data"
-
--- Given a type name, returns a list of its type constructor names tupled with
--- the number of arguments they take.
-typeCons :: Name -> Q [(Name,Int)]
-typeCons t = do
-  ti <- reify t
-  return . map simplify $ case ti of
-    TyConI (DataD    _ _ _ cs _) -> cs
-    TyConI (NewtypeD _ _ _ c  _) -> [c]
-    _ -> error $ "error (typeConstructors): symbol "
-              ++ show t
-              ++ " is neither newtype nor data"
-  where simplify (NormalC n ts)  = (n,length ts)
-        simplify (RecC    n ts)  = (n,length ts)
-        simplify (InfixC  _ n _) = (n,2)
-
--- Append to instance contexts in a declaration.
---
--- > sequence [[|Eq b|],[|Eq c|]] |=>| [t|instance Eq a => Cl (Ty a) where f=g|]
--- > == [t| instance (Eq a, Eq b, Eq c) => Cl (Ty a) where f = g |]
-(|=>|) :: Cxt -> DecsQ -> DecsQ
-c |=>| qds = do ds <- qds
-                return $ map (`ac` c) ds
-  where ac (InstanceD c ts ds) c' = InstanceD (c++c') ts ds
-        ac d                   _  = d
diff --git a/Test/Check/Error.hs b/Test/Check/Error.hs
deleted file mode 100644
--- a/Test/Check/Error.hs
+++ /dev/null
@@ -1,118 +0,0 @@
--- | A simple property-based testing library based on
---   enumeration of values via lists of lists.
---
--- This module re-exports Test.Check but some test functions have been
--- specialized to catch errors (see the explicit export list below).
---
--- This module is unsafe, it uses `unsafePerformIO` to catch errors.
-{-# LANGUAGE CPP #-}
-module Test.Check.Error
-  ( holds
-  , fails
-  , exists
-  , counterExample
-  , counterExamples
-  , witness
-  , witnesses
-  , results
-
-  , errorToNothing
-  , errorToFalse
-  , errorToTrue
-  , anyErrorToNothing
-
-  , module Test.Check
-  )
-where
-
-#if __GLASGOW_HASKELL__ <= 704
-import Prelude hiding (catch)
-#endif
-
-import Test.Check hiding
-  ( holds
-  , fails
-  , exists
-  , counterExample
-  , counterExamples
-  , witness
-  , witnesses
-  , results
-  )
-
-import qualified Test.Check as C
-  ( holds
-  , fails
-  , results
-  )
-
-import Control.Monad (liftM)
-import System.IO.Unsafe (unsafePerformIO)
-import Data.Maybe (listToMaybe)
-import Control.Exception ( Exception
-                         , SomeException
-                         , ArithException
-                         , ArrayException
-                         , ErrorCall
-                         , PatternMatchFail
-                         , catch
-                         , catches
-                         , Handler (Handler)
-                         , evaluate
-                         )
-
--- | Takes a value and a function.  Ignores the value.  Binds the argument of
---   the function to the type of the value.
-bindArgumentType :: a -> (a -> b) -> a -> b
-bindArgumentType _ f = f
-
--- | Transforms a value into 'Just' that value or 'Nothing' on some errors:
---
---   * ArithException
---   * ArrayException
---   * ErrorCall
---   * PatternMatchFail
-errorToNothing :: a -> Maybe a
-errorToNothing x = unsafePerformIO $
-  (Just `liftM` evaluate x) `catches` map ($ return Nothing)
-                                      [ hf (undefined :: ArithException)
-                                      , hf (undefined :: ArrayException)
-                                      , hf (undefined :: ErrorCall)
-                                      , hf (undefined :: PatternMatchFail)
-                                      ]
-  where hf :: Exception e => e -> IO a -> Handler a -- handlerFor
-        hf e h = Handler $ bindArgumentType e (\_ -> h)
-
--- | Transforms a value into 'Just' that value or 'Nothing' on error.
-anyErrorToNothing :: a -> Maybe a
-anyErrorToNothing x = unsafePerformIO $
-  (Just `liftM` evaluate x) `catch` \e -> do let _ = e :: SomeException
-                                             return Nothing
-
-errorToFalse :: Bool -> Bool
-errorToFalse p = case errorToNothing p of
-                   Just p' -> p
-                   Nothing -> False
-
-errorToTrue :: Bool -> Bool
-errorToTrue p = case errorToNothing p of
-                  Just p' -> p
-                  Nothing -> True
-
-
-holds,fails,exists :: Testable a => Int -> a -> Bool
-holds n = errorToFalse . C.holds n
-fails n = errorToTrue  . C.fails n
-exists n = or . take n . map snd . results
-
-counterExample,witness :: Testable a => Int -> a -> Maybe [String]
-counterExample n = listToMaybe . counterExamples n
-witness        n = listToMaybe . witnesses n
-
-counterExamples,witnesses :: Testable a => Int -> a -> [[String]]
-counterExamples n = map fst . filter (not . snd) . take n . results
-witnesses       n = map fst . filter snd         . take n . results
-
-results :: Testable a => a -> [([String],Bool)]
-results = map (mapSnd errorToFalse) . C.results
-  where mapSnd f (x,y) = (x,f y)
diff --git a/Test/Check/Function.hs b/Test/Check/Function.hs
deleted file mode 100644
--- a/Test/Check/Function.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-module Test.Check.Function () where
-import Test.Check.Function.ListsOfPairs ()
diff --git a/Test/Check/Function/CoListable.hs b/Test/Check/Function/CoListable.hs
deleted file mode 100644
--- a/Test/Check/Function/CoListable.hs
+++ /dev/null
@@ -1,65 +0,0 @@
--- | Function enumeration via CoListable typeclass
---   This currently just a sketch.
-module Test.Check.Function.CoListable
-where
-
-
-import Test.Check.Core
-import Test.Check.Utils
-import Data.Maybe (fromMaybe)
-
-
-(\+:/) :: [[a]] -> [[a]] -> [[a]]
-xss \+:/ yss = xss \/ ([]:yss)
-infixr 9 \+:/
-
-
-class CoListable a where
-  coListing :: [[b]] -> [[a -> b]]
-
-
-instance CoListable () where
-  coListing rs = mapT (\r  () -> r) rs
-
-
-instance CoListable Bool where
-  coListing rs = productWith (\r1 r2  b -> if b then r1 else r2) rs rs
-
-
-instance CoListable a => CoListable (Maybe a) where
-  coListing rs = productWith (\z f  m -> case m of Nothing -> z
-                                                   Just x  -> f x) rs (coListing rs)
-
-
-instance (CoListable a, CoListable b) => CoListable (Either a b) where
-  coListing rs = productWith (\f g  e -> case e of Left x  -> f x
-                                                   Right x -> g x) (coListing rs) (coListing rs)
-
-
-instance (CoListable a) => CoListable [a] where
-  coListing rss = mapT const rss
-             \+:/ productWith (\y f  xs -> case xs of []      -> y
-                                                      (x:xs') -> f x xs') rss (coListing (coListing rss))
-
-
-instance CoListable Int where
-  coListing rss = mapT const rss
-             \+:/ product3With (\f g z  i -> if i > 0 then f (i-1)
-                                        else if i < 0 then g (i+1)
-                                             else z) (coListing rss) (coListing rss) rss
-
-
-alts0 :: [[a]] -> [[a]]
-alts0 = id
-
-alts1 :: CoListable a => [[b]] -> [[a->b]]
-alts1 bs = coListing bs
-
-alts2 :: (CoListable a, CoListable b) => [[c]] -> [[a->b->c]]
-alts2 cs = coListing (coListing cs)
-
-alts3 :: (CoListable a, CoListable b, CoListable c) => [[d]] -> [[a->b->c->d]]
-alts3 ds = coListing (coListing (coListing ds))
-
-fListing :: (CoListable a, Listable b) => [[a->b]]
-fListing = coListing tiers
diff --git a/Test/Check/Function/ListsOfPairs.hs b/Test/Check/Function/ListsOfPairs.hs
deleted file mode 100644
--- a/Test/Check/Function/ListsOfPairs.hs
+++ /dev/null
@@ -1,62 +0,0 @@
--- | Function enumeration via lists of pairs.
-module Test.Check.Function.ListsOfPairs
-  ( functionPairs
-  , associations
-  , pairsToFunction
-  , defaultFunPairsToFunction
-  )
-where
-
-import Test.Check.Core
-import Test.Check.Utils
-import Data.Maybe (fromMaybe)
-
-instance (Eq a, Listable a, Listable b) => Listable (a -> b) where
-  tiers = mapT (uncurry $ flip defaultPairsToFunction)
-        $ functions list tiers
-
-
-functions :: [[a]] -> [[b]] -> [[([(a,b)],b)]]
-functions xss yss =
-  concatMapT
-    (\(r,yss) -> mapT (\ps -> (ps,r)) $ functionPairs xss yss)
-    (choices yss)
-
-
--- | Given a list of domain values, and tiers of codomain values,
--- return tiers of lists of ordered pairs of domain and codomain values.
---
--- Technically: tiers of left-total functional relations.
-associations :: [a] -> [[b]] -> [[ [(a,b)] ]]
-associations xs sbs = zip xs `mapT` products (const sbs `map` xs)
-
--- | Given tiers of input values and tiers of output values,
--- return tiers with all possible lists of input-output pairs.
--- Those represent functional relations.
-functionPairs :: [[a]] -> [[b]] -> [[[(a,b)]]]
-functionPairs xss yss = concatMapT (`associations` yss)
-                                   (strictlyAscendingListsOf xss)
-
--- | Returns a function given by a list of input-output pairs.
--- The result is wrapped in a maybe value.
--- The output for bound inputs is 'Just' a value.
--- The output for unbound inputs is 'Nothing'.
-pairsToMaybeFunction :: Eq a => [(a,b)] -> a -> Maybe b
-pairsToMaybeFunction []          _ = Nothing
-pairsToMaybeFunction ((a',r):bs) a | a == a'   = Just r
-                                   | otherwise = pairsToMaybeFunction bs a
-
--- | Returns a partial function given by a list of input-output pairs.
---
--- NOTE: This function *will* return undefined values for unbound inputs.
-pairsToFunction :: Eq a => [(a,b)] -> a -> b
-pairsToFunction bs a = fromMaybe undefined (pairsToMaybeFunction bs a)
-
-
--- | Returns a function given by a list of input-output pairs and a default value.
-defaultPairsToFunction :: Eq a => b -> [(a,b)] -> a -> b
-defaultPairsToFunction r bs a = fromMaybe r (pairsToMaybeFunction bs a)
-
-
-defaultFunPairsToFunction :: Eq a => (a -> b) -> [(a,b)] -> a -> b
-defaultFunPairsToFunction f bs a = fromMaybe (f a) (pairsToMaybeFunction bs a)
diff --git a/Test/Check/Function/Periodic.hs b/Test/Check/Function/Periodic.hs
deleted file mode 100644
--- a/Test/Check/Function/Periodic.hs
+++ /dev/null
@@ -1,47 +0,0 @@
--- | Periodic function enumeration.
---   This is just a sketch.
-module Test.Check.Function.Periodic
-where
-
-
-import Test.Check.Basic
-import Test.Check.Utils (listsOf)
-import Data.List (inits)
-
-
-instance (Eq a, Eq b, Listable a, Listable b) => Listable (a -> b) where
-  tiers = mapT pairsToFunction $ functions list tiers
-
-functions :: Eq b => [a] -> [[b]] -> [[[(a,b)]]]
-functions xs yss = mapT (zip xs . cycle) $ lsPeriodsOfLimit xs yss
-
-functionsz :: Eq b => [[a]] -> [[b]] -> [[[(a,b)]]]
-functionsz xss = functions (concat xss)
-
-
-lsPeriodsOf :: Eq a => [[a]] -> [[[a]]]
-lsPeriodsOf xss = map (filter isPeriod) (listsOf xss)
-
-lsPeriodsOfLimit :: Eq a => [b] -> [[a]] -> [[[a]]]
-lsPeriodsOfLimit ys xss = map (filter isPeriod) (tiersOfLimit ys xss)
-
-
-isPeriod :: Eq a => [a] -> Bool
-isPeriod [] = False
-isPeriod [x] = True
-isPeriod xs = not $ any (`isPeriodOf` xs) $ (tail . init . inits) xs
-
-isPeriodOf :: Eq a => [a] -> [a] -> Bool
-xs `isPeriodOf` ys = length ys `mod` length xs == 0
-                  && and (zipWith (==) (cycle xs) ys)
-
-
-tiersOfLimit :: [b] -> [[a]] -> [[[a]]]
-tiersOfLimit     [] xss = [[[]]]
-tiersOfLimit (_:ys) xss = [[[]]] ++ productWith (:) xss (tiersOfLimit ys xss)
-
-
-pairsToFunction :: Eq a => [(a,b)] -> (a -> b)
-pairsToFunction ((x,y):ps) x' =  if x' == x
-                                   then y
-                                   else pairsToFunction ps x'
diff --git a/Test/Check/Function/Show.hs b/Test/Check/Function/Show.hs
deleted file mode 100644
--- a/Test/Check/Function/Show.hs
+++ /dev/null
@@ -1,10 +0,0 @@
--- | A 'Show' instance for functions.
-module Test.Check.Function.Show () where
-
-import Test.Check.ShowFunction
-
-instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
-  showsPrec 0 = (++) . showFunction 8
-  showsPrec _ = (++) . paren . showFunctionLine 4
-    where paren s = "(" ++ s ++ ")"
-
diff --git a/Test/Check/IO.hs b/Test/Check/IO.hs
deleted file mode 100644
--- a/Test/Check/IO.hs
+++ /dev/null
@@ -1,80 +0,0 @@
--- | QuickCheck-like interface to LeanCheck
-{-# LANGUAGE CPP #-}
-module Test.Check.IO
-  ( check
-  , checkFor
-  , checkResult
-  , checkResultFor
-  )
-where
-
-#if __GLASGOW_HASKELL__ <= 704
-import Prelude hiding (catch)
-#endif
-
-import Test.Check.Core
-import Data.Maybe (listToMaybe)
-import Data.List (find)
-import Control.Exception (SomeException, catch, evaluate)
-
--- | Check a property
---   printing results on 'stdout'
-check :: Testable a => a -> IO ()
-check p = checkResult p >> return ()
-
--- | Check a property for @N@ tests
---   printing results on 'stdout'
-checkFor :: Testable a => Int -> a -> IO ()
-checkFor n p = checkResultFor n p >> return ()
-
--- | Check a property
---   printing results on 'stdout' and
---   returning 'True' on success.
---
--- There is no option to silence this function:
--- in that case, you should use 'Test.Check.holds'.
-checkResult :: Testable a => a -> IO Bool
-checkResult p = checkResultFor 200 p
-
--- | Check a property for @N@ tests
---   printing results on 'stdout' and
---   returning 'True' on success.
---
--- There is no option to silence this function:
--- in that case, you should use 'Test.Check.holds'.
-checkResultFor :: Testable a => Int -> a -> IO Bool
-checkResultFor n p = do
-  r <- resultIO n p
-  putStrLn . showResult $ r
-  return (isOK r)
-  where isOK (OK _) = True
-        isOK _      = False
-
-data Result = OK        Int
-            | Falsified Int [String]
-            | Exception Int [String] String
-  deriving (Eq, Show)
-
-resultsIO :: Testable a => Int -> a -> IO [Result]
-resultsIO n = sequence . zipWith torio [1..] . take n . results
-  where
-    tor i (_,True) = OK i
-    tor i (as,False) = Falsified i as
-    torio i r@(as,_) = evaluate (tor i r)
-       `catch` \e -> let _ = e :: SomeException
-                     in return (Exception i as (show e))
-
-resultIO :: Testable a => Int -> a -> IO Result
-resultIO n p = do
-  rs <- resultsIO n p
-  return . maybe (last rs) id
-         $ find isFailure rs
-  where isFailure (OK _) = False
-        isFailure _      = True
-
-showResult :: Result -> String
-showResult (OK n)             = "+++ OK, passed " ++ show n ++ " tests."
-showResult (Falsified i ce)   = "*** Failed! Falsifiable (after "
-                             ++ show i ++ " tests):\n" ++ unwords ce
-showResult (Exception i ce e) = "*** Failed! Exception '" ++ e ++ "' (after "
-                             ++ show i ++ " tests):\n" ++ unwords ce
diff --git a/Test/Check/Invariants.hs b/Test/Check/Invariants.hs
deleted file mode 100644
--- a/Test/Check/Invariants.hs
+++ /dev/null
@@ -1,130 +0,0 @@
--- | Some invariants over Test.Check functions
---   You should be importing this ONLY to test 'Check.hs' itself.
-module Test.Check.Invariants
-  ( tNatPairOrd
-  , tNatTripleOrd
-  , tNatQuadrupleOrd
-  , tNatQuintupleOrd
-  , tNatSixtupleOrd
-  , tNatListOrd
-  , tListsOfNatOrd
-  , tPairEqParams
-  , tTripleEqParams
-  , tProductsIsFilterByLength
-
-  , ordered
-  , orderedBy
-  , strictlyOrdered
-  , strictlyOrderedBy
-  )
-where
-
-import Test.Check
-import Data.List
-import Data.Ord
-import Test.Types (Nat(..))
-
--- | check if a list is ordered
-ordered :: Ord a => [a] -> Bool
-ordered = orderedBy compare
--- ordered [] = True
--- ordered [_] = True
--- ordered (x:y:xs) = x <= y && ordered (y:xs)
-
-strictlyOrdered :: Ord a => [a] -> Bool
-strictlyOrdered = strictlyOrderedBy compare
-
--- | check if a list is ordered by a given ordering function
-orderedBy :: (a -> a -> Ordering) -> [a] -> Bool
-orderedBy _ [] = True
-orderedBy _ [_] = True
-orderedBy cmp (x:y:xs) = case x `cmp` y of
-                           GT -> False
-                           _  -> orderedBy cmp (y:xs)
-
--- | check if a list is strictly ordered by a given ordering function
-strictlyOrderedBy :: (a -> a -> Ordering) -> [a] -> Bool
-strictlyOrderedBy _ [] = True
-strictlyOrderedBy _ [_] = True
-strictlyOrderedBy cmp (x:y:xs) = case x `cmp` y of
-                                   LT -> strictlyOrderedBy cmp (y:xs)
-                                   _  -> False
-
-ifNotEq :: Ordering -> Ordering -> Ordering
--- Could be implemented as:  ifNotEq = mappend
-ifNotEq EQ p = p
-ifNotEq  o _ = o
-
-thn :: (a->a->Ordering) -> (a->a->Ordering) -> a -> a -> Ordering
-thn cmp1 cmp2 x y = (x `cmp1` y) `ifNotEq` (x `cmp2` y)
-infixr 9 `thn`
-
-
--- | checks if the first 'n' elements on tiers are ordered by 'cmp'.
---
--- > (n `seriesOrderedBy`) comparing (id :: Type)
-tOrderedBy :: Listable a => Int -> (a -> a -> Ordering) -> Bool
-tOrderedBy n cmp = orderedBy cmp $ take n list
-infixr 9 `tOrderedBy`
-
-tStrictlyOrderedBy :: Listable a => Int -> (a -> a -> Ordering) -> Bool
-tStrictlyOrderedBy n cmp = strictlyOrderedBy cmp $ take n list
-infixr 9 `tStrictlyOrderedBy`
-
-tNatPairOrd :: Int -> Bool
-tNatPairOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
-  where sum' (x,y) = x+y :: Nat
-
-tNatTripleOrd :: Int -> Bool
-tNatTripleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
-  where sum' (x,y,z) = x+y+z :: Nat
-
-tNatQuadrupleOrd :: Int -> Bool
-tNatQuadrupleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
-  where sum' (x,y,z,w) = x+y+z+w :: Nat
-
-tNatQuintupleOrd :: Int -> Bool
-tNatQuintupleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
-  where sum' (x,y,z,w,v) = x+y+z+w+v :: Nat
-
-tNatSixtupleOrd :: Int -> Bool
-tNatSixtupleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
-  where sum' (x,y,z,w,v,u) = x+y+z+w+v+u :: Nat
-
-tNatListOrd :: Int -> Bool
-tNatListOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
-  where sum' = sum . map (+1) :: [Nat] -> Nat
-
-tListsOfStrictlyOrderedBy :: Int
-                           -> (a -> a -> Ordering)
-                           -> [[a]]
-                           -> Bool
-tListsOfStrictlyOrderedBy n cmp = strictlyOrderedBy cmp . take n . concat
-infixr 9 `tListsOfStrictlyOrderedBy`
-
-tListsOfNatOrd :: Int -> Bool
-tListsOfNatOrd n = tListsOfStrictlyOrderedBy n (comparing sum' `thn` compare) tiers
-  where sum' = sum . map (+1) :: [Nat] -> Nat
-
-tPairEqParams :: Int -> Bool
-tPairEqParams n = ces == srs
-  where
-    ces = map (map read) $ counterExamples n fail
-    srs = map pairToList $ take n list
-    pairToList (x,y) = [x,y :: Nat]
-    fail :: Nat -> Nat -> Bool
-    fail x y = False
-
-tTripleEqParams :: Int -> Bool
-tTripleEqParams n = ces == srs
-  where
-    ces = map (map read) $ counterExamples n fail
-    srs = map tripleToList $ take n list
-    tripleToList (x,y,z) = [x,y,z :: Nat]
-    fail :: Nat -> Nat -> Nat -> Bool
-    fail x y z = False
-
-tProductsIsFilterByLength :: Eq a => [[a]] -> Int -> Int -> Bool
-tProductsIsFilterByLength values m n = concat (take m byProduct) `isPrefixOf` concat byFilter
-  where byProduct = products $ replicate n values
-        byFilter  = ((==n) . length) `filterT` listsOf values
diff --git a/Test/Check/ShowFunction.hs b/Test/Check/ShowFunction.hs
deleted file mode 100644
--- a/Test/Check/ShowFunction.hs
+++ /dev/null
@@ -1,173 +0,0 @@
--- | This module exports the 'ShowFunction' typeclass,
---   its instances and related functions.
---
--- Using this module, it is possible to implement
--- a Show instance for functions:
---
--- > import Test.Check.ShowFunction
--- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
--- >   show = showFunction 8
---
--- This shows functions as a case pattern with up to 8 cases.
---
--- The module
--- @Test.Check.Function.Show@ ('Test.Check.Function.Show')
--- exports an instance like the one above.
-module Test.Check.ShowFunction
-  ( showFunction
-  , showFunctionLine
-  , Binding
-  , bindings
-  , ShowFunction (..)
-  , tBindingsShow
-  -- * Re-exports
-  , Listable
-  )
-where
-
-import Test.Check.Core
-import Test.Check.Error (errorToNothing)
-import Data.List
-import Data.Maybe
-
--- | A functional binding in a showable format.
-type Binding = ([String], Maybe String)
-
--- | 'ShowFunction' values are those for which
---   we can return a list of functional bindings.
---
--- As a user, you probably want 'showFunction' and 'showFunctionLine'.
---
--- Non functional instances should be defined by:
---
--- > instance ShowFunction Ty where tBindings = tBindingsShow
-class ShowFunction a where
-  tBindings :: a -> [[Binding]]
-
--- | Given a 'ShowFunction' value, return a list of bindings
---   for printing.  Examples:
---
--- > bindings True == [([],True)]
--- > bindings (id::Int) == [(["0"],"0"), (["1"],"1"), (["-1"],"-1"), ...
--- > bindings (&&) == [ (["False","False"], "False")
--- >                  , (["False","True"], "False")
--- >                  , (["True","False"], "False")
--- >                  , (["True","True"], "True")
--- >                  ]
-bindings :: ShowFunction a => a -> [Binding]
-bindings = concat . tBindings
-
-
--- instances for (algebraic/numeric) data types --
--- | A default implementation of tBindings for already 'Show'-able types.
-tBindingsShow :: Show a => a -> [[Binding]]
-tBindingsShow x = [[([],errorToNothing $ show x)]]
-
-instance ShowFunction ()   where tBindings = tBindingsShow
-instance ShowFunction Bool where tBindings = tBindingsShow
-instance ShowFunction Int  where tBindings = tBindingsShow
-instance ShowFunction Char where tBindings = tBindingsShow
-instance Show a => ShowFunction [a]       where tBindings = tBindingsShow
-instance Show a => ShowFunction (Maybe a) where tBindings = tBindingsShow
-instance (Show a, Show b) => ShowFunction (a,b) where tBindings = tBindingsShow
-
-
--- instance for functional value type --
-instance (Show a, Listable a, ShowFunction b) => ShowFunction (a->b) where
-  tBindings f = concatMapT tBindingsFor tiers
-    where tBindingsFor x = mapFst (show x:) `mapT` tBindings (f x)
-          mapFst f (x,y) = (f x, y)
-
-paren :: String -> String
-paren s = "(" ++ s ++ ")"
-
-varnamesFor :: ShowFunction a => a -> [String]
-varnamesFor = zipWith const varnames . fst . head . bindings
-  where varnames = ["x","y","z","w"] ++ map (++"'") varnames
-
-showTuple :: [String] -> String
-showTuple [x] = x
-showTuple xs  = paren $ intercalate "," xs
-
-showNBindingsOf :: ShowFunction a => Int -> Int -> a -> [String]
-showNBindingsOf m n f = take n bs
-                     ++ ["..." | length bs' >= m || length bs > n]
-  where bs' = take m $ bindings f
-        bs = [ showTuple as ++ " -> " ++ r
-             | (as, Just r) <- bs' ]
-
-isValue :: ShowFunction a => a -> Bool
-isValue f = case bindings f of
-              [([],_)] -> True
-              _        -> False
-
-showValueOf :: ShowFunction a => a -> String
-showValueOf x = case snd . head . bindings $ x of
-                  Nothing -> "undefined"
-                  Just x' -> x'
-
--- | Given a number of patterns to show, shows a 'ShowFunction' value.
---
--- > showFunction undefined True == "True"
--- > showFunction 3 (id::Int) == "\\x -> case x of\n\
--- >                              \        0 -> 0\n\
--- >                              \        1 -> 1\n\
--- >                              \        -1 -> -1\n\
--- >                              \        ...\n"
--- > showFunction 4 (&&) == "\\x y -> case (x,y) of\n\
--- >                         \          (False,False) -> False\n\
--- >                         \          (False,True) -> False\n\
--- >                         \          (True,False) -> False\n\
--- >                         \          (True,True) -> True\n"
---
--- This can be used as an implementation of show for functions:
---
--- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
--- >   show = showFunction 8
-showFunction :: ShowFunction a => Int -> a -> String
-showFunction n = showFunctionL False (n*n+1) n
-
--- | Same as showFunction, but has no line breaks.
---
--- > showFunction 2 (id::Int) == "\\x -> case x of 0 -> 0; 1 -> 1; ..."
-showFunctionLine :: ShowFunction a => Int -> a -> String
-showFunctionLine n = showFunctionL True (n*n+1) n
-
--- | isUndefined checks if a function is totally undefined.
--- When it is not possible to check all values, it returns false
-isUndefined :: ShowFunction a => Int -> a -> Bool
-isUndefined m f = length bs < m && all (isNothing . snd) bs
-  where bs = take m $ bindings f
-
--- The first boolean parameter tells if we are showing
--- the function on a single line
-showFunctionL :: ShowFunction a => Bool -> Int -> Int -> a -> String
-showFunctionL singleLine m n f | isValue f = showValueOf f
-showFunctionL singleLine m n f | otherwise = lambdaPat ++ caseExp
-  where
-    vs = varnamesFor f
-    lambdaPat = "\\" ++ unwords vs ++ " -> "
-    casePat = "case " ++ showTuple vs ++ " of"
-    bs = showNBindingsOf m n f
-    sep | singleLine = " "
-        | otherwise = "\n"
-    cases | singleLine = intercalate "; " bs
-          | otherwise  = unlines
-                       $ (replicate (length lambdaPat + 2) ' ' ++) `map` bs
-    caseExp = if isUndefined m f
-                then "undefined"
-                else casePat ++ sep ++ cases
-
--- instances for further tuples --
-instance (Show a, Show b, Show c)
-      => ShowFunction (a,b,c) where tBindings = tBindingsShow
-instance (Show a, Show b, Show c, Show d)
-      => ShowFunction (a,b,c,d) where tBindings = tBindingsShow
-instance (Show a, Show b, Show c, Show d, Show e)
-      => ShowFunction (a,b,c,d,e) where tBindings = tBindingsShow
-instance (Show a, Show b, Show c, Show d, Show e, Show f)
-      => ShowFunction (a,b,c,d,e,f) where tBindings = tBindingsShow
-instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g)
-      => ShowFunction (a,b,c,d,e,f,g) where tBindings = tBindingsShow
-instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g, Show h)
-      => ShowFunction (a,b,c,d,e,f,g,h) where tBindings = tBindingsShow
diff --git a/Test/Check/Utils.hs b/Test/Check/Utils.hs
deleted file mode 100644
--- a/Test/Check/Utils.hs
+++ /dev/null
@@ -1,232 +0,0 @@
--- | Utilities functions for manipulating tiers (sized lists of lists)
-module Test.Check.Utils
-  (
-  -- * Additional tiers constructors
-    consFromList
-  , consFromAscendingList
-  , consFromStrictlyAscendingList
-  , consFromSet
-  , consFromNoDupList
-
-  -- * Products of tiers
-  , product3With
-  , productMaybeWith
-
-  -- * Tiers of lists
-  , listsOf
-  , ascendingListsOf
-  , strictlyAscendingListsOf
-  , setsOf
-  , noDupListsOf
-  , products
-  , listsOfLength
-
-  , deleteT
-  , normalizeT
-
-  -- * Tiers of choices
-  , choices
-  , ascendingChoices
-  , strictlyAscendingChoices
-  )
-where
-
-import Test.Check.Basic
-import Data.Maybe (catMaybes)
-
--- | Given a constructor for a type that takes a list,
---   return tiers for that type.
-consFromList :: Listable a => ([a] -> b) -> [[b]]
-consFromList = (`mapT` listsOf tiers)
-
-consFromAscendingList :: Listable a => ([a] -> b) -> [[b]]
-consFromAscendingList = (`mapT` ascendingListsOf tiers)
-
--- | Given a constructor for a type that takes a list with strictly ascending
---   elements, return tiers of that type (e.g.: a Set type).
-consFromStrictlyAscendingList :: Listable a => ([a] -> b) -> [[b]]
-consFromStrictlyAscendingList = (`mapT` strictlyAscendingListsOf tiers)
-
--- | Given a constructor for a type that takes a set of elements (as a list)
---   return tiers of that type (e.g.: a Set type).
-consFromSet :: Listable a => ([a] -> b) -> [[b]]
-consFromSet = (`mapT` setsOf tiers)
-
--- | Given a constructor for a type that takes a list with no duplicate
---   elements, return tiers of that type.
-consFromNoDupList :: Listable a => ([a] -> b) -> [[b]]
-consFromNoDupList f = mapT f (noDupListsOf tiers)
-
-
--- | Like 'product', but over 3 lists of tiers.
-product3With :: (a->b->c->d) -> [[a]] -> [[b]] -> [[c]] -> [[d]]
-product3With f xss yss zss = productWith ($) (productWith f xss yss) zss
-
--- | Take the product of lists of tiers by a function returning a maybe value.
-productMaybeWith :: (a->b->Maybe c) -> [[a]] -> [[b]] -> [[c]]
-productMaybeWith _ _ [] = []
-productMaybeWith _ [] _ = []
-productMaybeWith f (xs:xss) yss = map (xs **) yss
-                               \/ productMaybeWith f xss yss `addWeight` 1
-  where xs ** ys = catMaybes [ f x y | x <- xs, y <- ys ]
-
-
--- | Given tiers of values, returns tiers of lists of those values
---
--- > listsOf [[]] == [[[]]]
---
--- > listsOf [[x]] == [ [[]]
--- >                  , [[x]]
--- >                  , [[x,x]]
--- >                  , [[x,x,x]]
--- >                  , ...
--- >                  ]
---
--- > listsOf [[x],[y]] == [ [[]]
--- >                      , [[x]]
--- >                      , [[x,x],[y]]
--- >                      , [[x,x,x],[x,y],[y,x]]
--- >                      , ...
--- >                      ]
-listsOf :: [[a]] -> [[[a]]]
-listsOf xss = cons0 []
-           \/ productWith (:) xss (listsOf xss) `addWeight` 1
-
--- | Generates several lists of the same size.
---
--- > products [ xss, yss, zss ] ==
---
--- Tiers of all lists combining elements of tiers: xss, yss and zss
-products :: [ [[a]] ] -> [[ [a] ]]
-products = foldr (productWith (:)) [[[]]]
-
--- | Delete the first occurence of an element in a tier,
---   for tiers without repetitions:
---
--- > deleteT x === normalizeT . (`suchThat` (/= x))
-deleteT :: Eq a => a -> [[a]] -> [[a]]
-deleteT _ [] = []
-deleteT y ([]:xss) = [] : deleteT y xss
-deleteT y [[x]]        | x == y    = []
-deleteT y ((x:xs):xss) | x == y    = xs:xss
-                       | otherwise = [[x]] \/ deleteT y (xs:xss)
-
-normalizeT :: [[a]] -> [[a]]
-normalizeT [] = []
-normalizeT [[]] = []
-normalizeT (xs:xss) = xs:normalizeT xss
-
--- | Given tiers of values, returns tiers of lists with no repeated elements.
---
--- > noDupListsOf [[0],[1],[2],...] ==
--- >   [ [[]]
--- >   , [[0]]
--- >   , [[1]]
--- >   , [[0,1],[1,0],[2]]
--- >   , [[0,2],[2,0],[3]]
--- >   , ...
--- >   ]
-noDupListsOf :: [[a]] -> [[[a]]]
-noDupListsOf =
-  ([[]]:) . concatT . choicesWith (\x xss -> mapT (x:) (noDupListsOf xss))
-
--- | Lists tiers of all choices of values from tiers.
--- Choices are pairs of values and tiers excluding that value.
---
--- > choices [[False,True]] == [[(False,[[True]]),(True,[[False]])]]
--- > choices [[1],[2],[3]]
--- >   == [ [(1,[[],[2],[3]])]
--- >      , [(2,[[1],[],[3]])]
--- >      , [(3,[[1],[2],[]])] ]
---
--- Each choice is sized by the extracted element.
-choices :: [[a]] -> [[(a,[[a]])]]
-choices = choicesWith (,)
-
--- | Like 'choices', but allows a custom function.
-choicesWith :: (a -> [[a]] -> b) -> [[a]] -> [[b]]
-choicesWith f []           = []
-choicesWith f [[]]         = []
-choicesWith f ([]:xss)     = [] : choicesWith (\y yss -> f y ([]:yss)) xss
-choicesWith f ((x:xs):xss) = [[f x (xs:xss)]]
-                          \/ choicesWith (\y (ys:yss) -> f y ((x:ys):yss)) (xs:xss)
-
--- | Given tiers of values,
---   returns tiers of lists of elements in ascending order
---                               (from tiered enumeration).
---
-ascendingListsOf :: [[a]] -> [[[a]]]
-ascendingListsOf =
-  ([[]]:) . concatT . ascendingChoicesWith (\x xss -> mapT (x:) (ascendingListsOf xss))
-
--- > ascendingChoices [[False,True]] =
--- >   [ [(False,[[False,True]]), (True,[[True]])]
--- >   ]
---
--- > ascendingChoices [[1],[2],[3],...] =
--- >   [ [(1,[[1],[2],[3],...])]
--- >   , [(2,[[ ],[2],[3],...])]
--- >   , [(3,[[ ],[ ],[3],...])]
--- >   , ...
--- >   ]
-ascendingChoices :: [[a]] -> [[(a,[[a]])]]
-ascendingChoices = ascendingChoicesWith (,)
-
-ascendingChoicesWith :: (a -> [[a]] -> b) -> [[a]] -> [[b]]
-ascendingChoicesWith f []           = []
-ascendingChoicesWith f [[]]         = []
-ascendingChoicesWith f ([]:xss)     = [] : ascendingChoicesWith (\y yss -> f y ([]:yss)) xss
-ascendingChoicesWith f ((x:xs):xss) = [[f x ((x:xs):xss)]]
-                                   \/ ascendingChoicesWith f (xs:xss)
-
--- | Given tiers of values,
---   returns tiers of lists of elements in strictly ascending order
---                              (from tiered enumeration).
---   If you only care about whether elements are in returned lists,
---   this returns the tiers of all sets of values.
---
--- > strictlyAscendingListsOf [[0],[1],[2],...] ==
--- >   [ [[]]
--- >   , [[0]]
--- >   , [[1]]
--- >   , [[0,1],[2]]
--- >   , [[0,2],[3]]
--- >   , [[0,3],[1,2],[4]]
--- >   , [[0,1,2],[0,4],[1,3],[5]]
--- >   , ...
--- >   ]
-strictlyAscendingListsOf :: [[a]] -> [[[a]]]
-strictlyAscendingListsOf =
-  ([[]]:) . concatT .
-  strictlyAscendingChoicesWith
-    (\x xss -> mapT (x:) (strictlyAscendingListsOf xss))
-
--- | Returns tiers of sets represented as lists of values (no repeated sets).
---   Shorthand for 'strictlyAscendingListsOf'.
-setsOf :: [[a]] -> [[[a]]]
-setsOf = strictlyAscendingListsOf
-
--- | Like 'choices', but paired tiers are always strictly ascending (in terms
---   of enumeration).
---
--- > strictlyAscendingChoices [[False,True]] == [[(False,[[True]]),(True,[[]])]]
--- > strictlyAscendingChoices [[1],[2],[3]]
--- >   == [ [(1,[[],[2],[3]])]
--- >      , [(2,[[],[],[3]])]
--- >      , [(3,[[],[],[]])]
--- >      ]
-strictlyAscendingChoices :: [[a]] -> [[(a,[[a]])]]
-strictlyAscendingChoices = strictlyAscendingChoicesWith (,)
-
--- | Like 'strictlyAscendingChoices' but customized by a function.
-strictlyAscendingChoicesWith :: (a -> [[a]] -> b) -> [[a]] -> [[b]]
-strictlyAscendingChoicesWith f []           = []
-strictlyAscendingChoicesWith f [[]]         = []
-strictlyAscendingChoicesWith f ([]:xss)     = [] : strictlyAscendingChoicesWith (\y yss -> f y ([]:yss)) xss
-strictlyAscendingChoicesWith f ((x:xs):xss) = [[f x (xs:xss)]]
-                                           \/ strictlyAscendingChoicesWith f (xs:xss)
-
-
--- | Given tiers, returns tiers of lists of a given length.
-listsOfLength :: Int -> [[a]] -> [[[a]]]
-listsOfLength n xss = products (replicate n xss)
diff --git a/Test/Most.hs b/Test/Most.hs
deleted file mode 100644
--- a/Test/Most.hs
+++ /dev/null
@@ -1,21 +0,0 @@
--- | Simple property-based testing library
---   based on enumeration of values via lists of lists.
---
--- This module exports Most modules that accompain Test.Check
--- and is to be used as a shorthand:
---
--- > import Test.Most
---
--- To get most of the needed stuff
-module Test.Most
-  ( module Test.Check
-  , module Test.Operators
-  , module Test.TypeBinding
-  , module Test.Types
-  )
-where
-
-import Test.Check
-import Test.Operators
-import Test.TypeBinding
-import Test.Types
diff --git a/Test/Operators.hs b/Test/Operators.hs
deleted file mode 100644
--- a/Test/Operators.hs
+++ /dev/null
@@ -1,113 +0,0 @@
-module Test.Operators
-  (
---  (==>) -- already provided by Test.Check
-
-  -- * Combining properties
-    (===), (====)
-  , (&&&), (&&&&)
-  , (|||), (||||)
-
-  -- * Properties over functions
-  , commutative
-  , associative
-  , distributive
-  , transitive
-  , idempotent
-  , identity
-  , notIdentity
-
-  -- * Ternary comparison operators
-  , (=$), ($=)
-  , (=|), (|=)
-  )
-where
-
-import Test.Check ((==>))
-
-combine :: (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
-combine op f g = \x -> f x `op` g x
-
--- Uneeded, just food for thought
---combine2 :: (c -> d -> e) -> (a -> b -> c) -> (a -> b -> d) -> (a -> b -> e)
--- Two possible implementations:
---combine2 op f g = \x y -> f x y `op` g x y
---combine2 = combine . combine
-
-(===) :: Eq b => (a -> b) -> (a -> b) -> a -> Bool
-(===) = combine (==)
-infix 4 ===
-
-(====) :: Eq c => (a -> b -> c) -> (a -> b -> c) -> a -> b -> Bool
-(====) = combine (===)
-infix 4 ====
-
-(&&&) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
-(&&&) = combine (&&)
-infix 3 &&&
-
-(&&&&) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
-(&&&&) = combine (&&&)
-infix 3 &&&&
-
-(|||) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
-(|||) = combine (||)
-infix 2 |||
-
-(||||) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
-(||||) = combine (|||)
-infix 2 ||||
-
-commutative :: Eq b => (a -> a -> b) -> a -> a -> Bool
-commutative o = \x y -> x `o` y == y `o` x
-
-associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
-associative o = \x y z -> x `o` (y `o` z) == (x `o` y) `o` z
-
--- type could be more general: (b -> a -> a) for both operators
-distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
-distributive o o' = \x y z -> x `o` (y `o'` z) == (x `o` y) `o'` (x `o` z)
-
-transitive :: (a -> a -> Bool) -> a -> a -> a -> Bool
-transitive o = \x y z -> x `o` y && y `o` z ==> x `o` z
-
-idempotent :: Eq a => (a -> a) -> a -> Bool
-idempotent f = f . f === f
-
-identity :: Eq a => (a -> a) -> a -> Bool
-identity f = f === id
-
-notIdentity :: Eq a => (a -> a) -> a -> Bool
-notIdentity = (not .) . identity
-
--- | Equal under.  A ternary operator.
---
--- > x =$ f $= y  =  f x = f y
---
--- > [1,2,3,4,5] =$  take 2    $= [1,2,4,8,16] -- > True
--- > [1,2,3,4,5] =$  take 3    $= [1,2,4,8,16] -- > False
--- >     [1,2,3] =$    sort    $= [3,2,1]      -- > True
--- >          42 =$ (`mod` 10) $= 16842        -- > True
--- >          42 =$ (`mod`  9) $= 16842        -- > False
--- >         'a' =$  isLetter  $= 'b'          -- > True
--- >         'a' =$  isLetter  $= '1'          -- > False
-(=$) :: Eq b => a -> (a -> b) -> a -> Bool
-(x =$ f) y = f x == f y
-infixl 4 =$
-
-($=) :: (a -> Bool) -> a -> Bool
-($=) = ($)
-infixl 4 $=
-
--- | Check if two lists are equal for @n@ values.
---
--- > xs =| n |= ys  =  take n xs == take n ys
---
--- > [1,2,3,4,5] =| 2 |= [1,2,4,8,16] -- > True
--- > [1,2,3,4,5] =| 3 |= [1,2,4,8,16] -- > False
-(=|) :: Eq a => [a] -> Int -> [a] -> Bool
-xs =| n = xs =$ take n
-infixl 4 =|
-
-(|=) :: (a -> Bool) -> a -> Bool
-(|=) = ($)
-infixl 4 |=
diff --git a/Test/TypeBinding.hs b/Test/TypeBinding.hs
deleted file mode 100644
--- a/Test/TypeBinding.hs
+++ /dev/null
@@ -1,229 +0,0 @@
--- | Infix operators for type binding using dummy first-class values.
---
--- Those are useful when property based testing to avoid repetition.
--- Suppose:
---
--- > prop_sortAppend :: Ord a => [a] -> Bool
--- > prop_sortAppend xs =  sort (xs++ys) == sort (ys++xs)
---
--- Then this:
---
--- > testResults n =
--- >   [ holds n (prop_sortAppend :: [Int] -> [Int] -> Bool)
--- >   , holds n (prop_sortAppend :: [UInt2] -> [UInt2] -> Bool)
--- >   , holds n (prop_sortAppend :: [Bool] -> [Bool] -> Bool)
--- >   , holds n (prop_sortAppend :: [Char] -> [Char] -> Bool)
--- >   , holds n (prop_sortAppend :: [String] -> [String] -> Bool)
--- >   , holds n (prop_sortAppend :: [()] -> [()] -> Bool)
--- >   ]
---
--- Becomes this:
---
--- > testResults n =
--- >   [ holds n $ prop_sortAppend -:> [int]
--- >   , holds n $ prop_sortAppend -:> [uint2]
--- >   , holds n $ prop_sortAppend -:> [bool]
--- >   , holds n $ prop_sortAppend -:> [char]
--- >   , holds n $ prop_sortAppend -:> [string]
--- >   , holds n $ prop_sortAppend -:> [()]
--- >   ]
---
--- Or even:
---
--- > testResults n = concat
--- >   [ for int, for uint2, for bool, for (), for char, for string ]
--- >   where for a = [ holds n $ prop_sortAppend -:> a ]
---
--- This last form is useful when testing multiple properties for multiple
--- types.
-module Test.TypeBinding
-  (
-  -- * Type binding operators
-  --
-  -- | Summary:
-  --
-  -- *                 as type of: '-:'
-  -- *        argument as type of: '-:>'
-  -- *          result as type of: '->:'
-  -- * second argument as type of: '->:>'
-  -- * second  result  as type of: '->>:'
-  -- * third  argument as type of: '->>:>'
-  -- * third   result  as type of: '->>>:'
-    (-:)
-  , (-:>)
-  , (->:)
-  , (->:>)
-  , (->>:)
-  , (->>:>)
-  , (->>>:)
-
-  -- * Dummy (undefined) values
-  -- ** Standard Haskell types
-  , und
-  , (>-)
-  , bool
-  , int, integer
-  , float, double
-  , char, string
-  , mayb, eith
-  -- ** Testing types
-  , nat
-  , int1, uint1
-  , int2, uint2
-  , int3, uint3
-  , int4, uint4
-  )
-where
-
-import Test.Types
-
-undefinedOf :: String -> a
-undefinedOf fn = error $ "Test.TypeBinding." ++ fn
-
--- | Type restricted version of const
--- that forces its first argument
--- to have the same type as the second.
--- A symnonym to 'asTypeOf':
---
--- >  value -: ty  =  value :: Ty
---
--- Examples:
---
--- >  10 -: int   =  10 :: Int
--- >  undefined -: 'a' >- 'b'  =  undefined :: Char -> Char
-(-:) :: a -> a -> a
-(-:) = asTypeOf -- const
-infixl 1 -:
-
--- | Type restricted version of const
--- that forces the argument of its first argument
--- to have the same type as the second:
---
--- >  f -:> ty  =  f -: ty >- und  =  f :: Ty -> a
---
--- Example:
---
--- >  abs -:> int   =  abs -: int >- und  =  abs :: Int -> Int
-(-:>) :: (a -> b) -> a -> (a -> b)
-(-:>) = const
-infixl 1 -:>
-
--- | Type restricted version of const
--- that forces the result of its first argument
--- to have the same type as the second.
---
--- >  f ->: ty  =  f -: und >- ty  =  f :: a -> Ty
-(->:) :: (a -> b) -> b -> (a -> b)
-(->:) = const
-infixl 1 ->:
-
--- | Type restricted version of const
--- that forces the second argument of its first argument
--- to have the same type as the second.
---
--- > f ->:> ty   =  f -: und -> ty -> und  =  f :: a -> Ty -> b
-(->:>) :: (a -> b -> c) -> b -> (a -> b -> c)
-(->:>) = const
-infixl 1 ->:>
-
--- | Type restricted version of const
--- that forces the result of the result of its first argument
--- to have the same type as the second.
---
--- > f ->>: ty   =  f -: und -> und -> ty  =  f :: a -> b -> Ty
-(->>:) :: (a -> b -> c) -> c -> (a -> b -> c)
-(->>:) = const
-infixl 1 ->>:
-
--- | Type restricted version of const
--- that forces the third argument of its first argument
--- to have the same type as the second.
-(->>:>) :: (a -> b -> c -> d) -> c -> (a -> b -> c -> d)
-(->>:>) = const
-infixl 1 ->>:>
-
--- | Type restricted version of const
--- that forces the result of the result of the result of its first argument
--- to have the same type as the second.
-(->>>:) :: (a -> b -> c -> d) -> d -> (a -> b -> c -> d)
-(->>>:) = const
-infixl 1 ->>>:
-
--- | Returns an undefined functional value
--- that takes an argument of the type of its first argument
--- and return a value of the type of its second argument.
---
--- > ty >- ty  =  (undefined :: Ty -> Ty)
---
--- Examples:
---
--- > 'a' >- 'b'  =  char >- char  =  (undefined :: Char -> Char)
--- > int >- bool >- int  =  undefined :: Int -> Bool -> Int
-(>-) :: a -> b -> (a -> b)
-(>-) = undefinedOf "(>-): undefined function -- using dummy value?"
-infixr 9 >-
-
-
--- Dummy values of standard Haskell types
-
--- | Shorthand for undefined
-und :: a
-und = undefinedOf "und"
-
-int :: Int
-int = undefinedOf "int"
-
-integer :: Integer
-integer = undefinedOf "integer"
-
-float :: Float
-float = undefinedOf "float"
-
-double :: Double
-double = undefinedOf "double"
-
-bool :: Bool
-bool = undefinedOf "bool"
-
-char :: Char
-char = undefinedOf "char"
-
-string :: String
-string = undefinedOf "string"
-
--- | It might be better to just use 'Just'
-mayb :: a -> Maybe a
-mayb = undefinedOf "mayb"
-
-eith :: a -> b -> Either a b
-eith = undefinedOf "eith"
-
-
--- Dummy values of Test.Types's types:
-
-nat :: Nat
-nat = undefinedOf "nat"
-
-int1 :: Int1
-int1 = undefinedOf "int1"
-
-int2 :: Int2
-int2 = undefinedOf "int2"
-
-int3 :: Int3
-int3 = undefinedOf "int3"
-
-int4 :: Int4
-int4 = undefinedOf "int4"
-
-uint1 :: UInt1
-uint1 = undefinedOf "uint1"
-
-uint2 :: UInt2
-uint2 = undefinedOf "uint2"
-
-uint3 :: UInt3
-uint3 = undefinedOf "uint3"
-
-uint4 :: UInt4
-uint4 = undefinedOf "uint4"
diff --git a/Test/Types.hs b/Test/Types.hs
deleted file mode 100644
--- a/Test/Types.hs
+++ /dev/null
@@ -1,438 +0,0 @@
--- | Types to aid in property-based testing.
-module Test.Types
-  (
-  -- * Integer types
-  --
-  -- | Small-width integer types to aid in property-based testing.
-  -- Sometimes it is useful to limit the possibilities of enumerated values
-  -- when testing polymorphic functions, these types allow that.
-  --
-  -- The signed integer types @IntN@ are of limited bit width @N@
-  -- bounded by @-2^(N-1)@ to @2^(N-1)-1@.
-  -- The unsigned integer types @WordN@ are of limited bit width @N@
-  -- bounded by @0@ to @2^N-1@.
-  --
-  -- Operations are closed and modulo @2^N@.  e.g.:
-  --
-  -- > maxBound + 1      = minBound
-  -- > read "2"          = -2 :: Int2
-  -- > abs minBound      = minBound
-  -- > negate n          = 2^N - n :: WordN
-    Int1
-  , Int2
-  , Int3
-  , Int4
-  , Word1
-  , Word2
-  , Word3
-  , Word4
-  , Nat
-  , Nat1
-  , Nat2
-  , Nat3
-  , Nat4
-  , Nat5
-  , Nat6
-  , Nat7
-
-  -- * Aliases to word types (deprecated)
-  , UInt1
-  , UInt2
-  , UInt3
-  , UInt4
-  )
-where
--- TODO: Add Ix and Bits instances
-
-import Test.Check (Listable(..), listIntegral)
-import Data.Ratio ((%))
-
-narrowU :: Int -> Int -> Int
-narrowU w i = i `mod` 2^w
-
-narrowS :: Int -> Int -> Int
-narrowS w i = let l  = 2^w
-                  i' = i `mod` l
-              in if i' < 2^(w-1)
-                   then i'
-                   else i' - l
-
-mapTuple :: (a -> b) -> (a,a) -> (b,b)
-mapTuple f (x,y) = (f x, f y)
-
-mapFst :: (a -> b) -> (a,c) -> (b,c)
-mapFst f (x,y) = (f x,y)
-
-oNewtype :: (a -> b) -> (b -> a) -> (a -> a -> a) -> (b -> b -> b)
-oNewtype con des o = \x y -> con $ des x `o` des y
-
-fNewtype :: (a -> b) -> (b -> a) -> (a -> a) -> (b -> b)
-fNewtype con des f = con . f . des
-
-otNewtype :: (a -> b) -> (b -> a) -> (a -> a -> (a,a)) -> (b -> b -> (b,b))
-otNewtype con des o = \x y -> mapTuple con $ des x `o` des y
-
-readsPrecNewtype :: Read a => (a -> b) -> Int -> String -> [(b,String)]
-readsPrecNewtype con n = map (mapFst con) . readsPrec n
-
-boundedEnumFrom :: (Ord a,Bounded a,Enum a) => a -> [a]
-boundedEnumFrom x = [x..maxBound]
-
-boundedEnumFromThen :: (Ord a,Bounded a,Enum a) => a -> a -> [a]
-boundedEnumFromThen x y | x > y     = [x,y..minBound]
-                        | otherwise = [x,y..maxBound]
-
--- | Single-bit signed integers: -1, 0
-newtype Int1 = Int1 { unInt1 :: Int } deriving (Eq, Ord)
-
--- | Two-bit signed integers: -2, -1, 0, 1
-newtype Int2 = Int2 { unInt2 :: Int } deriving (Eq, Ord)
-
--- | Three-bit signed integers: -4, -3, -2, -1, 0, 1, 2, 3
-newtype Int3 = Int3 { unInt3 :: Int } deriving (Eq, Ord)
-
--- | Four-bit signed integers:
--- -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7
-newtype Int4 = Int4 { unInt4 :: Int } deriving (Eq, Ord)
-
--- | Single-bit unsigned integer: 0, 1
-newtype Word1 = Word1 { unWord1 :: Int } deriving (Eq, Ord)
-
--- | Two-bit unsigned integers: 0, 1, 2, 3
-newtype Word2 = Word2 { unWord2 :: Int } deriving (Eq, Ord)
-
--- | Three-bit unsigned integers: 0, 1, 2, 3, 4, 5, 6, 7
-newtype Word3 = Word3 { unWord3 :: Int } deriving (Eq, Ord)
-
--- | Four-bit unsigned integers:
--- 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15
-newtype Word4 = Word4 { unWord4 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers (including 0): 0, 1, 2, 3, 4, 5, 6, 7, ...
---
--- Internally, this type is represented as an 'Int'.
--- So, it is limited by the 'maxBound' of 'Int'.
-newtype Nat = Nat { unNat :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 1: 0
-newtype Nat1 = Nat1 { unNat1 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 2: 0, 1
-newtype Nat2 = Nat2 { unNat2 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 3: 0, 1, 2
-newtype Nat3 = Nat3 { unNat3 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 4: 0, 1, 2, 3
-newtype Nat4 = Nat4 { unNat4 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 5: 0, 1, 2, 3, 4
-newtype Nat5 = Nat5 { unNat5 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 6: 0, 1, 2, 3, 4, 5
-newtype Nat6 = Nat6 { unNat6 :: Int } deriving (Eq, Ord)
-
--- | Natural numbers modulo 7: 0, 1, 2, 3, 4, 5, 6
-newtype Nat7 = Nat7 { unNat7 :: Int } deriving (Eq, Ord)
-
-int1  :: Int -> Int1;   int1  = Int1  . narrowS 1
-int2  :: Int -> Int2;   int2  = Int2  . narrowS 2
-int3  :: Int -> Int3;   int3  = Int3  . narrowS 3
-int4  :: Int -> Int4;   int4  = Int4  . narrowS 4
-word1 :: Int -> Word1;  word1 = Word1 . narrowU 1
-word2 :: Int -> Word2;  word2 = Word2 . narrowU 2
-word3 :: Int -> Word3;  word3 = Word3 . narrowU 3
-word4 :: Int -> Word4;  word4 = Word4 . narrowU 4
-nat1 :: Int -> Nat1;  nat1 = Nat1 . (`mod` 1)
-nat2 :: Int -> Nat2;  nat2 = Nat2 . (`mod` 2)
-nat3 :: Int -> Nat3;  nat3 = Nat3 . (`mod` 3)
-nat4 :: Int -> Nat4;  nat4 = Nat4 . (`mod` 4)
-nat5 :: Int -> Nat5;  nat5 = Nat5 . (`mod` 5)
-nat6 :: Int -> Nat6;  nat6 = Nat6 . (`mod` 6)
-nat7 :: Int -> Nat7;  nat7 = Nat7 . (`mod` 7)
-
-oInt1  ::(Int->Int->Int)->(Int1->Int1->Int1)   ; oInt1  = oNewtype int1  unInt1
-oInt2  ::(Int->Int->Int)->(Int2->Int2->Int2)   ; oInt2  = oNewtype int2  unInt2
-oInt3  ::(Int->Int->Int)->(Int3->Int3->Int3)   ; oInt3  = oNewtype int3  unInt3
-oInt4  ::(Int->Int->Int)->(Int4->Int4->Int4)   ; oInt4  = oNewtype int4  unInt4
-oWord1 ::(Int->Int->Int)->(Word1->Word1->Word1); oWord1 = oNewtype word1 unWord1
-oWord2 ::(Int->Int->Int)->(Word2->Word2->Word2); oWord2 = oNewtype word2 unWord2
-oWord3 ::(Int->Int->Int)->(Word3->Word3->Word3); oWord3 = oNewtype word3 unWord3
-oWord4 ::(Int->Int->Int)->(Word4->Word4->Word4); oWord4 = oNewtype word4 unWord4
-oNat   ::(Int->Int->Int)->(Nat->Nat->Nat)      ; oNat   = oNewtype Nat   unNat
-oNat1  ::(Int->Int->Int)->(Nat1->Nat1->Nat1)   ; oNat1  = oNewtype nat1  unNat1
-oNat2  ::(Int->Int->Int)->(Nat2->Nat2->Nat2)   ; oNat2  = oNewtype nat2  unNat2
-oNat3  ::(Int->Int->Int)->(Nat3->Nat3->Nat3)   ; oNat3  = oNewtype nat3  unNat3
-oNat4  ::(Int->Int->Int)->(Nat4->Nat4->Nat4)   ; oNat4  = oNewtype nat4  unNat4
-oNat5  ::(Int->Int->Int)->(Nat5->Nat5->Nat5)   ; oNat5  = oNewtype nat5  unNat5
-oNat6  ::(Int->Int->Int)->(Nat6->Nat6->Nat6)   ; oNat6  = oNewtype nat6  unNat6
-oNat7  ::(Int->Int->Int)->(Nat7->Nat7->Nat7)   ; oNat7  = oNewtype nat7  unNat7
-
-fInt1  :: (Int->Int) -> (Int1->Int1)   ; fInt1  = fNewtype int1  unInt1
-fInt2  :: (Int->Int) -> (Int2->Int2)   ; fInt2  = fNewtype int2  unInt2
-fInt3  :: (Int->Int) -> (Int3->Int3)   ; fInt3  = fNewtype int3  unInt3
-fInt4  :: (Int->Int) -> (Int4->Int4)   ; fInt4  = fNewtype int4  unInt4
-fWord1 :: (Int->Int) -> (Word1->Word1) ; fWord1 = fNewtype word1 unWord1
-fWord2 :: (Int->Int) -> (Word2->Word2) ; fWord2 = fNewtype word2 unWord2
-fWord3 :: (Int->Int) -> (Word3->Word3) ; fWord3 = fNewtype word3 unWord3
-fWord4 :: (Int->Int) -> (Word4->Word4) ; fWord4 = fNewtype word4 unWord4
-fNat   :: (Int->Int) -> (Nat->Nat)     ; fNat   = fNewtype Nat   unNat
-fNat1  :: (Int->Int) -> (Nat1->Nat1)   ; fNat1  = fNewtype nat1  unNat1
-fNat2  :: (Int->Int) -> (Nat2->Nat2)   ; fNat2  = fNewtype nat2  unNat2
-fNat3  :: (Int->Int) -> (Nat3->Nat3)   ; fNat3  = fNewtype nat3  unNat3
-fNat4  :: (Int->Int) -> (Nat4->Nat4)   ; fNat4  = fNewtype nat4  unNat4
-fNat5  :: (Int->Int) -> (Nat5->Nat5)   ; fNat5  = fNewtype nat5  unNat5
-fNat6  :: (Int->Int) -> (Nat6->Nat6)   ; fNat6  = fNewtype nat6  unNat6
-fNat7  :: (Int->Int) -> (Nat7->Nat7)   ; fNat7  = fNewtype nat7  unNat7
-
-instance Show Int1 where show = show . unInt1
-instance Show Int2 where show = show . unInt2
-instance Show Int3 where show = show . unInt3
-instance Show Int4 where show = show . unInt4
-instance Show Word1 where show = show . unWord1
-instance Show Word2 where show = show . unWord2
-instance Show Word3 where show = show . unWord3
-instance Show Word4 where show = show . unWord4
-instance Show Nat where show (Nat x) = show x
-instance Show Nat1 where show = show . unNat1
-instance Show Nat2 where show = show . unNat2
-instance Show Nat3 where show = show . unNat3
-instance Show Nat4 where show = show . unNat4
-instance Show Nat5 where show = show . unNat5
-instance Show Nat6 where show = show . unNat6
-instance Show Nat7 where show = show . unNat7
-
-instance Read Int1 where readsPrec = readsPrecNewtype int1
-instance Read Int2 where readsPrec = readsPrecNewtype int2
-instance Read Int3 where readsPrec = readsPrecNewtype int3
-instance Read Int4 where readsPrec = readsPrecNewtype int4
-instance Read Word1 where readsPrec = readsPrecNewtype word1
-instance Read Word2 where readsPrec = readsPrecNewtype word2
-instance Read Word3 where readsPrec = readsPrecNewtype word3
-instance Read Word4 where readsPrec = readsPrecNewtype word4
-instance Read Nat where readsPrec = readsPrecNewtype Nat
-instance Read Nat1 where readsPrec = readsPrecNewtype nat1
-instance Read Nat2 where readsPrec = readsPrecNewtype nat2
-instance Read Nat3 where readsPrec = readsPrecNewtype nat3
-instance Read Nat4 where readsPrec = readsPrecNewtype nat4
-instance Read Nat5 where readsPrec = readsPrecNewtype nat5
-instance Read Nat6 where readsPrec = readsPrecNewtype nat6
-instance Read Nat7 where readsPrec = readsPrecNewtype nat7
-
-
-instance Num Int1 where (+) = oInt1 (+);  abs    = fInt1 abs
-                        (-) = oInt1 (-);  signum = fInt1 signum
-                        (*) = oInt1 (*);  fromInteger = int1 . fromInteger
-
-instance Num Int2 where (+) = oInt2 (+);  abs    = fInt2 abs
-                        (-) = oInt2 (-);  signum = fInt2 signum
-                        (*) = oInt2 (*);  fromInteger = int2 . fromInteger
-
-instance Num Int3 where (+) = oInt3 (+);  abs    = fInt3 abs
-                        (-) = oInt3 (-);  signum = fInt3 signum
-                        (*) = oInt3 (*);  fromInteger = int3 . fromInteger
-
-instance Num Int4 where (+) = oInt4 (+);  abs    = fInt4 abs
-                        (-) = oInt4 (-);  signum = fInt4 signum
-                        (*) = oInt4 (*);  fromInteger = int4 . fromInteger
-
-instance Num Word1 where (+) = oWord1 (+);  abs    = fWord1 abs
-                         (-) = oWord1 (-);  signum = fWord1 signum
-                         (*) = oWord1 (*);  fromInteger = word1 . fromInteger
-
-instance Num Word2 where (+) = oWord2 (+);  abs    = fWord2 abs
-                         (-) = oWord2 (-);  signum = fWord2 signum
-                         (*) = oWord2 (*);  fromInteger = word2 . fromInteger
-
-instance Num Word3 where (+) = oWord3 (+);  abs    = fWord3 abs
-                         (-) = oWord3 (-);  signum = fWord3 signum
-                         (*) = oWord3 (*);  fromInteger = word3 . fromInteger
-
-instance Num Word4 where (+) = oWord4 (+);  abs    = fWord4 abs
-                         (-) = oWord4 (-);  signum = fWord4 signum
-                         (*) = oWord4 (*);  fromInteger = word4 . fromInteger
-
-instance Num Nat where (+) = oNat (+);  abs    = fNat abs
-                       (-) = oNat (-);  signum = fNat signum
-                       (*) = oNat (*);  fromInteger = Nat . fromInteger
-
-instance Num Nat1 where (+) = oNat1 (+);  abs    = fNat1 abs
-                        (-) = oNat1 (-);  signum = fNat1 signum
-                        (*) = oNat1 (*);  fromInteger = nat1 . fromInteger
-
-instance Num Nat2 where (+) = oNat2 (+);  abs    = fNat2 abs
-                        (-) = oNat2 (-);  signum = fNat2 signum
-                        (*) = oNat2 (*);  fromInteger = nat2 . fromInteger
-
-instance Num Nat3 where (+) = oNat3 (+);  abs    = fNat3 abs
-                        (-) = oNat3 (-);  signum = fNat3 signum
-                        (*) = oNat3 (*);  fromInteger = nat3 . fromInteger
-
-instance Num Nat4 where (+) = oNat4 (+);  abs    = fNat4 abs
-                        (-) = oNat4 (-);  signum = fNat4 signum
-                        (*) = oNat4 (*);  fromInteger = nat4 . fromInteger
-
-instance Num Nat5 where (+) = oNat5 (+);  abs    = fNat5 abs
-                        (-) = oNat5 (-);  signum = fNat5 signum
-                        (*) = oNat5 (*);  fromInteger = nat5 . fromInteger
-
-instance Num Nat6 where (+) = oNat6 (+);  abs    = fNat6 abs
-                        (-) = oNat6 (-);  signum = fNat6 signum
-                        (*) = oNat6 (*);  fromInteger = nat6 . fromInteger
-
-instance Num Nat7 where (+) = oNat7 (+);  abs    = fNat7 abs
-                        (-) = oNat7 (-);  signum = fNat7 signum
-                        (*) = oNat7 (*);  fromInteger = nat7 . fromInteger
-
-
-instance Real Int1 where toRational (Int1 x) = fromIntegral x % 1
-instance Real Int2 where toRational (Int2 x) = fromIntegral x % 1
-instance Real Int3 where toRational (Int3 x) = fromIntegral x % 1
-instance Real Int4 where toRational (Int4 x) = fromIntegral x % 1
-instance Real Word1 where toRational (Word1 x) = fromIntegral x % 1
-instance Real Word2 where toRational (Word2 x) = fromIntegral x % 1
-instance Real Word3 where toRational (Word3 x) = fromIntegral x % 1
-instance Real Word4 where toRational (Word4 x) = fromIntegral x % 1
-instance Real Nat where toRational (Nat x) = fromIntegral x % 1
-instance Real Nat1 where toRational (Nat1 x) = fromIntegral x % 1
-instance Real Nat2 where toRational (Nat2 x) = fromIntegral x % 1
-instance Real Nat3 where toRational (Nat3 x) = fromIntegral x % 1
-instance Real Nat4 where toRational (Nat4 x) = fromIntegral x % 1
-instance Real Nat5 where toRational (Nat5 x) = fromIntegral x % 1
-instance Real Nat6 where toRational (Nat6 x) = fromIntegral x % 1
-instance Real Nat7 where toRational (Nat7 x) = fromIntegral x % 1
-
-instance Integral Int1 where quotRem = otNewtype int1 unInt1 quotRem
-                             toInteger = toInteger . unInt1
-
-instance Integral Int2 where quotRem = otNewtype int2 unInt2 quotRem
-                             toInteger = toInteger . unInt2
-
-instance Integral Int3 where quotRem = otNewtype int3 unInt3 quotRem
-                             toInteger = toInteger . unInt3
-
-instance Integral Int4 where quotRem = otNewtype int4 unInt4 quotRem
-                             toInteger = toInteger . unInt4
-
-instance Integral Word1 where quotRem = otNewtype word1 unWord1 quotRem
-                              toInteger = toInteger . unWord1
-
-instance Integral Word2 where quotRem = otNewtype word2 unWord2 quotRem
-                              toInteger = toInteger . unWord2
-
-instance Integral Word3 where quotRem = otNewtype word3 unWord3 quotRem
-                              toInteger = toInteger . unWord3
-
-instance Integral Word4 where quotRem = otNewtype word4 unWord4 quotRem
-                              toInteger = toInteger . unWord4
-
-instance Integral Nat where quotRem = otNewtype Nat unNat quotRem
-                            toInteger = toInteger . unNat
-
-instance Integral Nat1 where quotRem = otNewtype nat1 unNat1 quotRem
-                             toInteger = toInteger . unNat1
-
-instance Integral Nat2 where quotRem = otNewtype nat2 unNat2 quotRem
-                             toInteger = toInteger . unNat2
-
-instance Integral Nat3 where quotRem = otNewtype nat3 unNat3 quotRem
-                             toInteger = toInteger . unNat3
-
-instance Integral Nat4 where quotRem = otNewtype nat4 unNat4 quotRem
-                             toInteger = toInteger . unNat4
-
-instance Integral Nat5 where quotRem = otNewtype nat5 unNat5 quotRem
-                             toInteger = toInteger . unNat5
-
-instance Integral Nat6 where quotRem = otNewtype nat6 unNat6 quotRem
-                             toInteger = toInteger . unNat6
-
-instance Integral Nat7 where quotRem = otNewtype nat7 unNat7 quotRem
-                             toInteger = toInteger . unNat7
-
-instance Bounded Int1 where maxBound = Int1 0; minBound = Int1 (-1)
-instance Bounded Int2 where maxBound = Int2 1; minBound = Int2 (-2)
-instance Bounded Int3 where maxBound = Int3 3; minBound = Int3 (-4)
-instance Bounded Int4 where maxBound = Int4 7; minBound = Int4 (-8)
-instance Bounded Word1 where maxBound = Word1 1; minBound = Word1 0
-instance Bounded Word2 where maxBound = Word2 3; minBound = Word2 0
-instance Bounded Word3 where maxBound = Word3 7; minBound = Word3 0
-instance Bounded Word4 where maxBound = Word4 15; minBound = Word4 0
-instance Bounded Nat1 where maxBound = Nat1 0; minBound = Nat1 0
-instance Bounded Nat2 where maxBound = Nat2 1; minBound = Nat2 0
-instance Bounded Nat3 where maxBound = Nat3 2; minBound = Nat3 0
-instance Bounded Nat4 where maxBound = Nat4 3; minBound = Nat4 0
-instance Bounded Nat5 where maxBound = Nat5 4; minBound = Nat5 0
-instance Bounded Nat6 where maxBound = Nat6 5; minBound = Nat6 0
-instance Bounded Nat7 where maxBound = Nat7 6; minBound = Nat7 0
-
-instance Enum Int1 where toEnum   = int1;   enumFrom     = boundedEnumFrom
-                         fromEnum = unInt1; enumFromThen = boundedEnumFromThen
-
-instance Enum Int2 where toEnum   = int2;   enumFrom     = boundedEnumFrom
-                         fromEnum = unInt2; enumFromThen = boundedEnumFromThen
-
-instance Enum Int3 where toEnum   = int3;   enumFrom     = boundedEnumFrom
-                         fromEnum = unInt3; enumFromThen = boundedEnumFromThen
-
-instance Enum Int4 where toEnum   = int4;   enumFrom     = boundedEnumFrom
-                         fromEnum = unInt4; enumFromThen = boundedEnumFromThen
-
-instance Enum Word1 where toEnum   = word1;   enumFrom     = boundedEnumFrom
-                          fromEnum = unWord1; enumFromThen = boundedEnumFromThen
-
-instance Enum Word2 where toEnum   = word2;   enumFrom     = boundedEnumFrom
-                          fromEnum = unWord2; enumFromThen = boundedEnumFromThen
-
-instance Enum Word3 where toEnum   = word3;   enumFrom     = boundedEnumFrom
-                          fromEnum = unWord3; enumFromThen = boundedEnumFromThen
-
-instance Enum Word4 where toEnum   = word4;   enumFrom     = boundedEnumFrom
-                          fromEnum = unWord4; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat where
-  toEnum   = Nat;    enumFrom     (Nat x)         = map Nat [x..]
-  fromEnum = unNat;  enumFromThen (Nat x) (Nat s) = map Nat [x,s..]
-
-instance Enum Nat1 where toEnum   = nat1;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat1; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat2 where toEnum   = nat2;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat2; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat3 where toEnum   = nat3;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat3; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat4 where toEnum   = nat4;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat4; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat5 where toEnum   = nat5;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat5; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat6 where toEnum   = nat6;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat6; enumFromThen = boundedEnumFromThen
-
-instance Enum Nat7 where toEnum   = nat7;   enumFrom     = boundedEnumFrom
-                         fromEnum = unNat7; enumFromThen = boundedEnumFromThen
-
-instance Listable Int1 where list = [0,minBound]
-instance Listable Int2 where list = listIntegral
-instance Listable Int3 where list = listIntegral
-instance Listable Int4 where list = listIntegral
-instance Listable Word1 where list = [0..]
-instance Listable Word2 where list = [0..]
-instance Listable Word3 where list = [0..]
-instance Listable Word4 where list = [0..]
-instance Listable Nat where list = [0..]
-instance Listable Nat1 where list = [0..]
-instance Listable Nat2 where list = [0..]
-instance Listable Nat3 where list = [0..]
-instance Listable Nat4 where list = [0..]
-instance Listable Nat5 where list = [0..]
-instance Listable Nat6 where list = [0..]
-instance Listable Nat7 where list = [0..]
-
-type UInt1 = Word1
-type UInt2 = Word2
-type UInt3 = Word3
-type UInt4 = Word4
diff --git a/doc/data-invariant.md b/doc/data-invariant.md
new file mode 100644
--- /dev/null
+++ b/doc/data-invariant.md
@@ -0,0 +1,73 @@
+Using LeanCheck types with a data invariant
+-------------------------------------------
+
+Some datatypes follow a data invariant / precondition, e.g.:
+  AVL and Red-Black trees must be balanced;
+  a [`Rational`] should be simplified and have a non-zero denominator;
+  a set representation by a list should be ordered.
+
+For the following `Set` datatype with insertion and membership test:
+
+    -- A simple set representation by a strictly ordered list
+    data Set a = Set [a]
+      deriving (Eq, Show)
+
+    -- data invariant for the Set type
+    okSet :: Ord a => Set a -> Bool
+    okSet (Set xs) = sord xs
+      where
+      sord (x:y:xs) = x < y && sord (y:xs)
+      sord _        = True
+
+    insertS :: Ord a => a -> Set a -> Set a
+    insertS x (Set xs) = Set $ insert x xs
+
+    elemS :: Ord a => a -> Set a -> Bool
+    elemS x (Set xs) = elem x xs
+
+By defining [`Listable`] naively
+
+    instance (Ord a, Listable a) => Listable (Set a) where
+      tiers = cons1 Set
+
+we get invalid sets when we [`list`] sets.  On ghci:
+
+    > take 5 (list :: [Set Int])
+    [Set [],Set [0],Set [0,0],Set [1],Set [0,0,0]]
+    > map okSet $ take 5 (list :: [Set Int])
+    [True,True,False,True,False]
+
+Both `Set [0,0]` and `Set [0,0,0]`, despite being type-correct, are invalid
+sets as they do not follow the data invariant `okSet`.  To resolve that, we
+have three solutions:
+
+1. **Prefix all properties with a precondition** (uglier and inefficient):
+
+        prop_elemInsertS :: Ord a => a -> Set a -> Bool
+        prop_elemInsertS x s = okSet s ==> x `elemS` (x `insertS` s)
+
+2. **Filter invalid values in the Listable instance** (elegant but inefficient):
+
+    We can use the [`suchThat`] function when declaring `tiers`:
+
+        instance (Ord a, Listable a) => Listable (Set a) where
+          tiers = cons1 Set `suchThat` okSet
+
+    Now only valid sets are listed:
+
+        > take 5 (list :: [Set Int])
+        [Set [],Set [0],Set [1],Set [0,1],Set [-1]]
+
+    And we can simply write our property as:
+
+        prop_elemInsertS x s = x `elemS` (x `insertS` s)
+
+
+3. **Only generate valid values in the Listable instance** (elegant and efficient):
+
+    TODO: write!
+
+[`Listable`]: https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#t:Listable
+[`list`]:     https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:list
+[`suchThat`]: https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:suchThat
+[`Rational`]: https://hackage.haskell.org/package/base/docs/Data-Ratio.html#t:Ratio
diff --git a/doc/tutorial.md b/doc/tutorial.md
new file mode 100644
--- /dev/null
+++ b/doc/tutorial.md
@@ -0,0 +1,271 @@
+Introduction to property-based testing (with LeanCheck)
+=======================================================
+
+This document introduces property-based testing.  The reader only needs to be
+familiar with Haskell.  No previous knowledge of property-based testing is
+assumed.  This document focuses on LeanCheck, but skills are transferable to
+[other property-based testing tools](#other-property-based-testing-tools-for-haskell).
+
+(If you are already familiar with property-based testing and just want to learn
+how to use LeanCheck, you might be best served by reading
+[LeanCheck's README file](../README.md).
+
+The learning outcomes of each section are:
+
+* [What is property-based testing?](#what-is-property-based-testing)
+  --- what is property-based testing;
+
+* [Example 1: testing `sort`](#example-1-testing-a-sort-implementation)
+  --- how to use a property-based testing library (LeanCheck);
+
+* [Example 2: testing `insert`](#example-2-testing-conditional-properties)
+  --- how to test conditional properties
+
+* [Example 3: testing `Stack`](#example-3-testing-user-defined-datatypes)
+  --- how to apply property-based testing to functions over user-defined
+  datatypes by declaring [`Listable`] typeclass instances;
+
+
+What is property-based testing?
+-------------------------------
+
+In property-based testing, properties are defined as Haskell functions
+returning a boolean value which should be `True` for all possible choices of
+argument values.  These properties are applied enumerated or random argument
+values in search for a counterexample.  This is perhaps better illustrated in
+an example (see Example 1).
+
+
+### Terminology
+
+Property-based testing might be known with other names:
+
+* property testing;
+* [parameterized unit tests]: in the context of C# ([NUnit]) or Java ([JUnit]),
+							  properties are viewed with unit tests with
+							  arguments.
+
+
+Example 1: testing a sort implementation
+----------------------------------------
+
+Lets imagine that we want to test an implementation of a (not-so-quick) `sort`
+function:
+
+    sort :: Ord a => [a] -> [a]
+    sort []     = []
+    sort (x:xs) = sort lesser ++ [x] ++ sort greater
+      where
+      lesser  = filter (< x) xs
+      greater = filter (> x) xs
+
+### In contrast --- unit testing
+
+We can *unit test* the above implementation:
+
+    testsPass  ::  Bool
+    testsPass = and
+      [ []       == sort ([]::[Int])
+      , [1]      == sort [1]
+      , [1,2,3]  == sort [1,2,3]
+      , [1,2,3]  == sort [3,2,1]
+      , [1..100] == sort [100,99..1]
+      ]
+
+If we evaluate `testsPass` on ghci, we will get `True` --- our implementation
+of `sort` passes all our unit tests.
+
+### Declaring properties
+
+Alternatively, we use *property-based testing* to test the above
+implementation.  We first declare a few properties:
+
+    prop_elem :: Ord a => a -> [a] -> Bool
+    prop_elem x xs =  elem x (sort xs) == elem x xs
+
+    prop_ordered :: Ord a => [a] -> Bool
+    prop_ordered xs =  ordered (sort xs)
+      where
+      ordered (x:y:xs) = x <= y && ordered (y:xs)
+      ordered _        = True
+
+    prop_length :: Ord a => [a] -> Bool
+	prop_length xs =  length (sort xs) == length xs
+
+Those properties are similar to unit tests, but are parameterized.  Instead of
+defining the behavior of sort for specific values, each property defines the
+behavior of `sort` for a range of values.
+
+### Testing properties
+
+By binding those properties to specific types and passing those properties as
+arguments to the [`check`] function, we get:
+
+    $ ghci
+	> import Test.Check
+
+    > check (prop_elem :: Int -> [Int] -> Bool)
+    +++ OK, passed 200 tests.
+
+    > check (prop_ordered :: [Int] -> Bool)
+    +++ OK, passed 200 tests.
+
+Internally, the function [`check`] enumerates arguments to those functions and
+test whether properties hold.
+
+### Finding and fixing bugs
+
+But what happens when the function does not follow the properties?
+
+    > check (prop_length :: [Int] -> Bool)
+    *** Failed! Falsifiable (after 3 tests):
+    [0,0]
+
+The `check` function reports a failing counterexample.  We get a `False` value
+when evaluating `prop_length [0,0]`.  We can investigate on GHCi:
+
+	> prop_length [0,0]
+	False
+	> length (sort [0,0]) == length [0,0]
+	False
+	> length (sort [0,0])
+	1
+	> sort [0,0]
+	[0]
+
+If we look back at our definition of `sort`, we can see that we forgot to
+account for repeated elements.  We should change `>` to `>=`:
+
+	greater = filter (>= x) xs
+
+After fixing that bug, `prop_length` will pass:
+
+    > check (prop_length :: [Int] -> Bool)
+    +++ OK, passed 200 tests.
+
+
+Example 2: testing conditional properties
+-----------------------------------------
+
+The boolean operator [`==>`] can be used to construct conditional properties.
+
+The function [`insert`] defined in [`Data.List`] inserts an element into a list
+at the first position where it is less than or equal to the next element.
+*If the list is already ordered, the resulting list will still be ordered:*
+
+    prop_insertOrd x xs =  ordered xs ==> ordered (insert x xs)
+
+
+Example 3: testing user-defined datatypes
+-----------------------------------------
+
+Consider the following implementation of a `Stack`:
+
+    data Stack a = Stack a (Stack a)
+                 | Empty
+      deriving (Show,Eq)
+
+    push :: a -> Stack a -> Stack a
+    push x s = Stack x s
+
+    pop :: Stack a -> (a, Stack a)
+    pop (Stack x s) = (x,s)
+
+We might want to test the following property:
+
+    prop_popush :: a -> Stack a -> Bool
+    prop_popush x s =  pop (push x s) == (x,s)
+
+However, if we provide this property on ghci, we get an error:
+
+    > check (prop_popush :: Int -> Stack Int -> Bool)
+    <interactive>:x:1:
+      No instance for (Listable (Stack Int))
+
+Our `Stack` type should be made an instance of the [`Listable`] typeclass.
+This way LeanCheck will have a way to know how to list values to be tested by
+the property.  See [`Listable`] documentation for more.  In this case, the
+instance is:
+
+    instance Listable a => Listable (Stack a) where
+      tiers = cons2 Stack
+           \/ cons0 Empty
+
+Now:
+
+    > check (prop_popush :: Int -> Stack Int -> Bool)
+    +++ OK, passed 200 tests.
+
+LeanCheck also provides the function [`deriveListable`] to automatically derive
+[`Listable`] instances for types that do not follow a data invariant (precondition).
+
+
+
+Advantages of property-based testing
+------------------------------------
+
+Property-based testing has a few advantages over unit-testing:
+
+* (+) scalability:
+  after making a small change to a program, we might [`checkFor`] `50` tests;
+  before making a major release, we may [`checkFor`] `1000` tests.
+  A continuous integration system can be configured to run more test than what
+  is usual on developers machines.
+  
+* (+) documentation:
+  properties serve as a clear documentation of behaviour;
+
+* (+) tool support:
+  in Haskell there are several different property-based testing tools to choose
+  from.
+
+
+The disadvantage is:
+
+* (-) Properties are comparatively harder to write than simple input and output
+  test cases. (+) However, it might be easier to define good properties than a good
+  selection of unit test cases.
+  See "[Ranking programs using Black-Box testing (2010)]".
+
+If you are unsure, you can always use *both* PBT and UT.
+
+
+Other property-based testing tools for Haskell
+----------------------------------------------
+
+* [QuickCheck]      : randomized
+* [SmallCheck]      : enumerative, depth-bounded
+* [Lazy SmallCheck] : enumerative, depth-bounded, lazy, demand-driven
+* [Feat]            : enumerative, size-bounded
+* [LeanCheck]       : enumerative, size-bounded
+
+
+Further reading
+---------------
+
+* [Using LeanCheck on functions over types with a data invariant](data-invariant.md)
+* [Testing and tracing using QuickCheck and Hat](https://www.cs.kent.ac.uk/pubs/2003/1896/content.pdf)
+* [QuickCheck's seminal paper (2000)](https://dl.acm.org/citation.cfm?id=1988046)
+* [SmallCheck's paper (2008)](http://dl.acm.org/citation.cfm?id=1411292)
+
+[`Listable`]:       https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#t:Listable
+[`check`]:          https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:check
+[`checkFor`]:       https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:checkFor
+[`==>`]:            https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:-61--61--62-
+[`deriveListable`]: https://hackage.haskell.org/package/leancheck/docs/Test-LeanCheck.html#v:deriveListable
+
+[QuickCheck]:      https://hackage.haskell.org/package/QuickCheck
+[SmallCheck]:      https://hackage.haskell.org/package/smallcheck
+[Lazy SmallCheck]: https://hackage.haskell.org/package/lazysmallcheck
+[Feat]:            https://hackage.haskell.org/package/testing-feat
+[LeanCheck]:       https://hackage.haskell.org/package/leancheck
+
+[parameterized unit tests]: http://research.microsoft.com/apps/pubs/default.aspx?id=77419
+[NUnit]: http://www.nunit.org/index.php?p=parameterizedTests&r=2.5
+[JUnit]: http://www.mkyong.com/unittest/junit-4-tutorial-6-parameterized-test/
+
+[`insert`]:    https://hackage.haskell.org/package/base/docs/Data-List.html#v:insert
+[`Data.List`]: https://hackage.haskell.org/package/base/docs/Data-List.html
+
+[Ranking programs using Black-Box testing (2010)]: http://www.cse.chalmers.se/~nicsma/papers/ranking-programs.pdf
+
diff --git a/leancheck.cabal b/leancheck.cabal
--- a/leancheck.cabal
+++ b/leancheck.cabal
@@ -2,32 +2,29 @@
 --
 -- Template Haskell dependency is optional.  To deactivate it:
 -- 1. In this file, comment out:
---   Test.Check.Derive
+--   Test.LeanCheck.Derive
 --   template-haskell
 --   and the test-suite derive
--- 2. On Test.Most, comment out the Test.Check.Derive module
--- 3. On Test.Check, comment out Test.Check.Derive and deriveListable
+-- 2. On Test.LeanCheck, comment out Test.LeanCheck.Derive and deriveListable
 --
 -- I could ultimately add a flag to deactivate that, but I do not want to make
 -- this cabal file too complicated.  -- Rudy
 
 name:                leancheck
-version:             0.3.0
+version:             0.4.0
 synopsis:            Cholesterol-free property-based testing
 description:
   LeanCheck is a simple enumerative property-based testing library.
   .
-  It works by producing *tiers* of test values,
-  which are essentially (possibly infinite) lists
-  of finite lists of same-and-increasingly-sized values.
+  Properties are defined as Haskell functions returning a boolean value which
+  should be true for all possible choices of argument values.    LeanCheck
+  applies enumerated argument values to these properties in search for a
+  counterexample.  Properties can be viewed as parameterized unit tests.
   .
-  LeanCheck has "lean" core with only 180 lines of Haskell code
-  but provides a selection of utilitites for property testing:
-  test types (@Nat@, @Nat\<1-7\>@, @Word\<1-4\>@, @Int\<1-4\>@);
-  test operators (@==>@, @===@, @&&&@, @|||@);
-  type binding operators.
+  LeanCheck works by producing tiers of test values: a possibly infinite list
+  of finite sublists of same-and-increasingly-sized values.
   .
-  LeanCheck API is likely to change in the near future.
+  LeanCheck has lean core with only 180 lines of Haskell code.
 
 homepage:            https://github.com/rudymatela/leancheck#readme
 license:             BSD3
@@ -38,8 +35,13 @@
 build-type:          Simple
 cabal-version:       >=1.10
 
-extra-source-files:  README.md, CREDITS.md
+extra-doc-files: README.md
+               , CREDITS.md
+               , doc/data-invariant.md
+               , doc/tutorial.md
+tested-with: GHC==7.10, GHC==7.8, GHC==7.6, GHC==7.4
 
+
 source-repository head
   type:            git
   location:        https://github.com/rudymatela/leancheck
@@ -47,75 +49,69 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/leancheck
-  tag:             v0.3.0
+  tag:             v0.4.0
 
 library
-  exposed-modules: Test.Check
-                 , Test.Check.Utils
-                 , Test.Check.Basic
-                 , Test.Check.Core
-                 , Test.Check.Derive
-                 , Test.Check.Error
-                 , Test.Check.IO
-                 , Test.Types
-                 , Test.Operators
-                 , Test.TypeBinding
-                 , Test.Most
-                 , Test.Check.Function
-                 , Test.Check.Function.ListsOfPairs
-                 , Test.Check.Function.CoListable
-                 , Test.Check.Function.Periodic
-                 , Test.Check.Function.Show
-                 , Test.Check.ShowFunction
-  other-modules:       Test.Check.Invariants
+  exposed-modules: Test.LeanCheck
+                 , Test.LeanCheck.Basic
+                 , Test.LeanCheck.Core
+                 , Test.LeanCheck.Derive
+                 , Test.LeanCheck.Error
+                 , Test.LeanCheck.IO
+                 , Test.LeanCheck.Tiers
+                 , Test.LeanCheck.Utils
+                 , Test.LeanCheck.Utils.Types
+                 , Test.LeanCheck.Utils.TypeBinding
+                 , Test.LeanCheck.Utils.Operators
+                 , Test.LeanCheck.Function
+                 , Test.LeanCheck.Function.ListsOfPairs
+                 , Test.LeanCheck.Function.CoListable
+                 , Test.LeanCheck.Function.Periodic
+                 , Test.LeanCheck.Function.Show
+                 , Test.LeanCheck.Function.ShowFunction
+  other-modules:       Test.LeanCheck.Invariants
+  hs-source-dirs:      src
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
 
 test-suite test
   type:                exitcode-stdio-1.0
   main-is:             test.hs
-  hs-source-dirs:      ., tests
+  hs-source-dirs:      src, tests
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
 
 test-suite types
   type:                exitcode-stdio-1.0
   main-is:             test-types.hs
-  hs-source-dirs:      ., tests
+  hs-source-dirs:      src, tests
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
 
 test-suite utils
   type:                exitcode-stdio-1.0
   main-is:             test-utils.hs
-  hs-source-dirs:      ., tests
+  hs-source-dirs:      src, tests
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
 
 test-suite operators
   type:                exitcode-stdio-1.0
   main-is:             test-operators.hs
-  hs-source-dirs:      ., tests
-  build-depends:       base >= 4 && < 5, template-haskell
-  default-language:    Haskell2010
-
-test-suite most
-  type:                exitcode-stdio-1.0
-  main-is:             test-most.hs
-  hs-source-dirs:      ., tests
+  hs-source-dirs:      src, tests
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
 
 test-suite derive
   type:                exitcode-stdio-1.0
-  main-is:             test-most.hs
-  hs-source-dirs:      ., tests
+  main-is:             test-derive.hs
+  hs-source-dirs:      src, tests
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
 
 test-suite error
   type:                exitcode-stdio-1.0
   main-is:             test-error.hs
-  hs-source-dirs:      ., tests
+  hs-source-dirs:      src, tests
   build-depends:       base >= 4 && < 5, template-haskell
   default-language:    Haskell2010
diff --git a/src/Test/LeanCheck.hs b/src/Test/LeanCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck.hs
@@ -0,0 +1,127 @@
+{-# OPTIONS_HADDOCK prune #-}
+-- | LeanCheck is a simple enumerative property-based testing library.
+--
+-- A __property__ is a function returning a 'Bool' that should be 'True' for
+-- all possible choices of arguments.  Properties can be viewed as a
+-- parameterized unit tests.
+--
+--
+-- To check if a property 'holds' by testing up to a thousand values,
+-- we evaluate:
+--
+-- > holds 1000 property
+--
+-- 'True' indicates success.  'False' indicates a bug.
+--
+-- For example:
+--
+-- > holds $ \xs -> length (sort xs) == length (xs::[Int])
+--
+--
+-- To get the smallest 'counterExample' by testing up to a thousand values,
+-- we evaluate:
+--
+-- > counterExample 1000 property
+--
+--
+-- Arguments of properties should be instances of the 'Listable' typeclass.
+-- 'Listable' instances are provided for the most common Haskell types.
+-- New instances are easily defined
+-- (see 'Listable' for more info).
+module Test.LeanCheck
+  (
+  -- * Checking and testing
+    holds
+  , fails
+  , exists
+
+  -- ** Boolean (property) operators
+  , (==>)
+
+  -- ** Counterexamples and witnesses
+  , counterExample
+  , counterExamples
+  , witness
+  , witnesses
+
+  -- ** Reporting
+  , check
+  , checkFor
+  , checkResult
+  , checkResultFor
+
+  -- * Listing test values
+  , Listable(..)
+
+  -- ** Listing constructors
+  , cons0
+  , cons1
+  , cons2
+  , cons3
+  , cons4
+  , cons5
+  , cons6
+  , cons7
+  , cons8
+  , cons9
+  , cons10
+  , cons11
+  , cons12
+
+  , ofWeight
+  , addWeight
+  , suchThat
+
+  -- ** Combining tiers
+  , (\/)
+  , (\\//)
+  , (><)
+  , productWith
+
+  -- ** Manipulating tiers
+  , mapT
+  , filterT
+  , concatT
+  , concatMapT
+  , deleteT
+  , normalizeT
+  , toTiers
+
+  -- ** Automatically deriving Listable instances
+  , deriveListable
+
+  -- ** Extra constructors
+  , consFromList
+  , consFromAscendingList
+  , consFromStrictlyAscendingList
+  , consFromSet
+  , consFromNoDupList
+
+  -- ** Products of tiers
+  , product3With
+  , productMaybeWith
+
+  -- * Listing lists
+  , listsOf
+  , setsOf
+  , ascendingListsOf
+  , strictlyAscendingListsOf
+  , noDupListsOf
+  , products
+  , listsOfLength
+
+  -- ** Listing values
+  , tiersFractional
+  , listIntegral
+  , (+|)
+
+  -- * Test results
+  , Testable
+  , results
+  )
+where
+
+import Test.LeanCheck.Basic
+import Test.LeanCheck.Tiers
+import Test.LeanCheck.Derive
+import Test.LeanCheck.IO
diff --git a/src/Test/LeanCheck/Basic.hs b/src/Test/LeanCheck/Basic.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Basic.hs
@@ -0,0 +1,123 @@
+-- | Simple property-based testing library based on
+--   enumeration of values via lists of lists.
+--
+-- This module exports "Test.LeanCheck.Core" functionality along with instances and
+-- functions for further tuple and constructor arities.
+--
+-- For the complete list of functions, see "Test.LeanCheck".
+module Test.LeanCheck.Basic
+  ( module Test.LeanCheck.Core
+
+  , cons6
+  , cons7
+  , cons8
+  , cons9
+  , cons10
+  , cons11
+  , cons12
+  )
+where
+
+import Test.LeanCheck.Core
+
+instance (Listable a, Listable b, Listable c,
+          Listable d, Listable e, Listable f) =>
+         Listable (a,b,c,d,e,f) where
+  tiers = productWith (\x (y,z,w,v,u) -> (x,y,z,w,v,u)) tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d,
+          Listable e, Listable f, Listable g) =>
+         Listable (a,b,c,d,e,f,g) where
+  tiers = productWith (\x (y,z,w,v,u,r) -> (x,y,z,w,v,u,r)) tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d,
+          Listable e, Listable f, Listable g, Listable h) =>
+         Listable (a,b,c,d,e,f,g,h) where
+  tiers = productWith (\x (y,z,w,v,u,r,s) -> (x,y,z,w,v,u,r,s))
+                      tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d, Listable e,
+          Listable f, Listable g, Listable h, Listable i) =>
+         Listable (a,b,c,d,e,f,g,h,i) where
+  tiers = productWith (\x (y,z,w,v,u,r,s,t) -> (x,y,z,w,v,u,r,s,t))
+                      tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d, Listable e,
+          Listable f, Listable g, Listable h, Listable i, Listable j) =>
+         Listable (a,b,c,d,e,f,g,h,i,j) where
+  tiers = productWith (\x (y,z,w,v,u,r,s,t,o) -> (x,y,z,w,v,u,r,s,t,o))
+                      tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d,
+          Listable e, Listable f, Listable g, Listable h,
+          Listable i, Listable j, Listable k) =>
+         Listable (a,b,c,d,e,f,g,h,i,j,k) where
+  tiers = productWith (\x (y,z,w,v,u,r,s,t,o,p) -> (x,y,z,w,v,u,r,s,t,o,p))
+                      tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d,
+          Listable e, Listable f, Listable g, Listable h,
+          Listable i, Listable j, Listable k, Listable l) =>
+         Listable (a,b,c,d,e,f,g,h,i,j,k,l) where
+  tiers = productWith (\x (y,z,w,v,u,r,s,t,o,p,q) ->
+                        (x,y,z,w,v,u,r,s,t,o,p,q))
+                      tiers tiers
+
+cons6 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f)
+      => (a -> b -> c -> d -> e -> f -> g) -> [[g]]
+cons6 f = mapT (uncurry6 f) tiers `addWeight` 1
+
+cons7 :: (Listable a, Listable b, Listable c, Listable d,
+          Listable e, Listable f, Listable g)
+      => (a -> b -> c -> d -> e -> f -> g -> h) -> [[h]]
+cons7 f = mapT (uncurry7 f) tiers `addWeight` 1
+
+cons8 :: (Listable a, Listable b, Listable c, Listable d,
+          Listable e, Listable f, Listable g, Listable h)
+      => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> [[i]]
+cons8 f = mapT (uncurry8 f) tiers `addWeight` 1
+
+cons9 :: (Listable a, Listable b, Listable c, Listable d, Listable e,
+          Listable f, Listable g, Listable h, Listable i)
+      => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> [[j]]
+cons9 f = mapT (uncurry9 f) tiers `addWeight` 1
+
+cons10 :: (Listable a, Listable b, Listable c, Listable d, Listable e,
+           Listable f, Listable g, Listable h, Listable i, Listable j)
+       => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> [[k]]
+cons10 f = mapT (uncurry10 f) tiers `addWeight` 1
+
+cons11 :: (Listable a, Listable b, Listable c, Listable d,
+           Listable e, Listable f, Listable g, Listable h,
+           Listable i, Listable j, Listable k)
+       => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> [[l]]
+cons11 f = mapT (uncurry11 f) tiers `addWeight` 1
+
+cons12 :: (Listable a, Listable b, Listable c, Listable d,
+           Listable e, Listable f, Listable g, Listable h,
+           Listable i, Listable j, Listable k, Listable l)
+       => (a->b->c->d->e->f->g->h->i->j->k->l->m) -> [[m]]
+cons12 f = mapT (uncurry12 f) tiers `addWeight` 1
+
+uncurry6 :: (a->b->c->d->e->f->g) -> (a,b,c,d,e,f) -> g
+uncurry6 f (x,y,z,w,v,u) = f x y z w v u
+
+uncurry7 :: (a->b->c->d->e->f->g->h) -> (a,b,c,d,e,f,g) -> h
+uncurry7 f (x,y,z,w,v,u,r) = f x y z w v u r
+
+uncurry8 :: (a->b->c->d->e->f->g->h->i) -> (a,b,c,d,e,f,g,h) -> i
+uncurry8 f (x,y,z,w,v,u,r,s) = f x y z w v u r s
+
+uncurry9 :: (a->b->c->d->e->f->g->h->i->j) -> (a,b,c,d,e,f,g,h,i) -> j
+uncurry9 f (x,y,z,w,v,u,r,s,t) = f x y z w v u r s t
+
+uncurry10 :: (a->b->c->d->e->f->g->h->i->j->k) -> (a,b,c,d,e,f,g,h,i,j) -> k
+uncurry10 f (x,y,z,w,v,u,r,s,t,o) = f x y z w v u r s t o
+
+uncurry11 :: (a->b->c->d->e->f->g->h->i->j->k->l)
+          -> (a,b,c,d,e,f,g,h,i,j,k) -> l
+uncurry11 f (x,y,z,w,v,u,r,s,t,o,p) = f x y z w v u r s t o p
+
+uncurry12 :: (a->b->c->d->e->f->g->h->i->j->k->l->m)
+          -> (a,b,c,d,e,f,g,h,i,j,k,l) -> m
+uncurry12 f (x,y,z,w,v,u,r,s,t,o,p,q) = f x y z w v u r s t o p q
diff --git a/src/Test/LeanCheck/Core.hs b/src/Test/LeanCheck/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Core.hs
@@ -0,0 +1,416 @@
+-- | Simple property-based testing library based on
+--   enumeration of values via lists of lists.
+--
+-- This is the core module of the library, with the most basic definitions.  If
+-- you are looking just to use the library, import and see "Test.LeanCheck".
+--
+-- If you want to understand how the code works, this is the place to start.
+--
+--
+-- Other important modules:
+--
+-- "Test.LeanCheck.Basic" re-exports (almost) everything from this module
+--         along with constructors and instances for further arities.
+--
+-- "Test.LeanCheck.Utils" re-exports "Test.LeanCheck.Basic"
+--         along with functions for advanced Listable instance definitions.
+--
+-- "Test.LeanCheck" re-exports "Test.LeanCheck.Utils"
+--   along with a TH function to automatically derive Listable instances.
+module Test.LeanCheck.Core
+  (
+  -- * Checking and testing
+    holds
+  , fails
+  , exists
+  , counterExample
+  , counterExamples
+  , witness
+  , witnesses
+  , Testable
+
+  , results
+
+  -- * Listing test values
+  , Listable(..)
+
+  -- ** Constructing lists of tiers
+  , cons0
+  , cons1
+  , cons2
+  , cons3
+  , cons4
+  , cons5
+
+  , ofWeight
+  , addWeight
+  , suchThat
+
+  -- ** Combining lists of tiers
+  , (\/), (\\//)
+  , (><)
+  , productWith
+
+  -- ** Manipulating lists of tiers
+  , mapT
+  , filterT
+  , concatT
+  , concatMapT
+  , toTiers
+
+  -- ** Boolean (property) operators
+  , (==>)
+
+  -- ** Misc utilities
+  , (+|)
+  , listIntegral
+  , tiersFractional
+  )
+where
+
+import Data.Maybe (listToMaybe)
+
+
+-- | A type is 'Listable' when there exists a function that
+--   is able to list (ideally all of) its values.
+--
+-- Ideally, instances should be defined by a 'tiers' function that
+-- returns a (potentially infinite) list of finite sub-lists (tiers):
+--   the first sub-list contains elements of size 0,
+--   the second sub-list contains elements of size 1
+--   and so on.
+-- Size here is defined by the implementor of the type-class instance.
+--
+-- For algebraic data types, the general form for 'tiers' is
+--
+-- > tiers = cons<N> ConstructorA
+-- >      \/ cons<N> ConstructorB
+-- >      \/ ...
+-- >      \/ cons<N> ConstructorZ
+--
+-- where @N@ is the number of arguments of each constructor @A...Z@.
+--
+-- Instances can be alternatively defined by 'list'.
+-- In this case, each sub-list in 'tiers' is a singleton list
+-- (each succeeding element of 'list' has +1 size).
+--
+-- The function 'Test.LeanCheck.Derive.deriveListable' from "Test.LeanCheck.Derive"
+-- can automatically derive instances of this typeclass.
+--
+-- A 'Listable' instance for functions is also available but is not exported by
+-- default.  Import "Test.LeanCheck.Function" if you need to test higher-order
+-- properties.
+class Listable a where
+  tiers :: [[a]]
+  list :: [a]
+  tiers = toTiers list
+  list = concat tiers
+  {-# MINIMAL list | tiers #-}
+
+-- | Takes a list of values @xs@ and transform it into tiers on which each
+--   tier is occupied by a single element from @xs@.
+--
+-- To convert back to a list, just 'concat'.
+toTiers :: [a] -> [[a]]
+toTiers = map (:[])
+
+instance Listable () where
+  list = [()]
+
+-- | Tiers of 'Integral' values.
+--   Can be used as a default implementation of 'list' for 'Integral' types.
+listIntegral :: (Enum a, Num a) => [a]
+listIntegral = [0,-1..] +| [1..]
+
+instance Listable Int where
+  list = listIntegral
+
+instance Listable Integer where
+  list = listIntegral
+
+instance Listable Char where
+  list = ['a'..'z']
+      +| [' ','\n']
+      +| ['A'..'Z']
+      +| ['0'..'9']
+      +| ['!'..'/']
+      +| ['\t']
+      +| [':'..'@']
+      +| ['['..'`']
+      +| ['{'..'~']
+
+instance Listable Bool where
+  tiers = cons0 False \/ cons0 True
+
+instance Listable a => Listable (Maybe a) where
+  tiers = cons0 Nothing \/ cons1 Just
+
+instance (Listable a, Listable b) => Listable (Either a b) where
+  tiers = cons1 Left  `ofWeight` 0
+     \\// cons1 Right `ofWeight` 0
+
+instance (Listable a, Listable b) => Listable (a,b) where
+  tiers = tiers >< tiers
+
+instance (Listable a, Listable b, Listable c) => Listable (a,b,c) where
+  tiers = productWith (\x (y,z) -> (x,y,z)) tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d) =>
+         Listable (a,b,c,d) where
+  tiers = productWith (\x (y,z,w) -> (x,y,z,w)) tiers tiers
+
+instance (Listable a, Listable b, Listable c, Listable d, Listable e) =>
+         Listable (a,b,c,d,e) where
+  tiers = productWith (\x (y,z,w,v) -> (x,y,z,w,v)) tiers tiers
+
+instance (Listable a) => Listable [a] where
+  tiers = cons0 []
+       \/ cons2 (:)
+
+-- | Tiers of 'Fractional' values.
+--   This can be used as the implementation of 'tiers' for 'Fractional' types.
+tiersFractional :: Fractional a => [[a]]
+tiersFractional = productWith (+) tiersFractionalParts
+                                  (mapT fromIntegral (tiers::[[Integer]]))
+               \/ [ [], [], [1/0], [-1/0] {- , [-0], [0/0] -} ]
+  where tiersFractionalParts :: Fractional a => [[a]]
+        tiersFractionalParts = [0]
+                             : [ [fromIntegral a / fromIntegral b]
+                               | b <- iterate (*2) 2, a <- [1::Integer,3..b] ]
+-- The position of Infinity in the above enumeration is arbitrary.
+
+-- Note that this instance ignores NaN's.
+instance Listable Float where
+  tiers = tiersFractional
+
+instance Listable Double where
+  tiers = tiersFractional
+
+
+-- | 'map' over tiers
+mapT :: (a -> b) -> [[a]] -> [[b]]
+mapT = map . map
+
+-- | 'filter' tiers
+filterT :: (a -> Bool) -> [[a]] -> [[a]]
+filterT f = map (filter f)
+
+-- | 'concat' tiers of tiers
+concatT :: [[ [[a]] ]] -> [[a]]
+concatT = foldr (\+:/) [] . map (foldr (\/) [])
+  where xss \+:/ yss = xss \/ ([]:yss)
+
+-- | 'concatMap' over tiers
+concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]]
+concatMapT f = concatT . mapT f
+
+
+-- | Given a constructor with no arguments,
+--   returns 'tiers' of all possible applications of this constructor.
+--   Since in this case there is only one possible application (to no
+--   arguments), only a single value, of size/weight 0, will be present in the
+--   resulting list of tiers.
+cons0 :: a -> [[a]]
+cons0 x = [[x]]
+
+-- | Given a constructor with one 'Listable' argument,
+--   return 'tiers' of applications of this constructor.
+--   By default, returned values will have size/weight of 1.
+cons1 :: Listable a => (a -> b) -> [[b]]
+cons1 f = mapT f tiers `addWeight` 1
+
+-- | Given a constructor with two 'Listable' arguments,
+--   return 'tiers' of applications of this constructor.
+--   By default, returned values will have size/weight of 1.
+cons2 :: (Listable a, Listable b) => (a -> b -> c) -> [[c]]
+cons2 f = mapT (uncurry f) tiers `addWeight` 1
+
+-- | Returns tiers of applications of a 3-argument constructor.
+cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]]
+cons3 f = mapT (uncurry3 f) tiers `addWeight` 1
+
+-- | Returns tiers of applications of a 4-argument constructor.
+cons4 :: (Listable a, Listable b, Listable c, Listable d)
+      => (a -> b -> c -> d -> e) -> [[e]]
+cons4 f = mapT (uncurry4 f) tiers `addWeight` 1
+
+-- | Returns tiers of applications of a 5-argument constructor.
+--
+-- "Test.LeanCheck.Basic" defines
+-- 'Test.LeanCheck.Basic.cons6' up to 'Test.LeanCheck.Basic.cons12'.
+-- Those are exported by default from "Test.LeanCheck",
+-- but are hidden from the Haddock documentation.
+cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e)
+      => (a -> b -> c -> d -> e -> f) -> [[f]]
+cons5 f = mapT (uncurry5 f) tiers `addWeight` 1
+
+-- | Resets the weight of a constructor (or tiers)
+-- Typically used as an infix constructor when defining Listable instances:
+--
+-- > cons<N> `ofWeight` <W>
+--
+-- Be careful: do not apply @`ofWeight` 0@ to recursive data structure
+-- constructors.  In general this will make the list of size 0 infinite,
+-- breaking the tier invariant (each tier must be finite).
+ofWeight :: [[a]] -> Int -> [[a]]
+ofWeight xss w = dropWhile null xss `addWeight` w
+
+-- | Adds to the weight of tiers of a constructor
+addWeight :: [[a]] -> Int -> [[a]]
+addWeight xss w = replicate w [] ++ xss
+
+-- | Tiers of values that follow a property
+--
+-- > cons<N> `suchThat` condition
+suchThat :: [[a]] -> (a->Bool) -> [[a]]
+suchThat = flip filterT
+
+-- | Lazily interleaves two lists, switching between elements of the two.
+--   Union/sum of the elements in the lists.
+--
+-- > [x,y,z] +| [a,b,c] == [x,a,y,b,z,c]
+(+|) :: [a] -> [a] -> [a]
+[]     +| ys = ys
+(x:xs) +| ys = x:(ys +| xs)
+infixr 5 +|
+
+-- | Append tiers --- sum of two tiers enumerations.
+--
+-- > [xs,ys,zs,...] \/ [as,bs,cs,...] = [xs++as,ys++bs,zs++cs,...]
+(\/) :: [[a]] -> [[a]] -> [[a]]
+xss \/ []  = xss
+[]  \/ yss = yss
+(xs:xss) \/ (ys:yss) = (xs ++ ys) : xss \/ yss
+infixr 7 \/
+
+-- | Interleave tiers --- sum of two tiers enumerations.
+--   When in doubt, use '\/' instead.
+--
+-- > [xs,ys,zs,...] \/ [as,bs,cs,...] = [xs+|as,ys+|bs,zs+|cs,...]
+(\\//) :: [[a]] -> [[a]] -> [[a]]
+xss \\// []  = xss
+[]  \\// yss = yss
+(xs:xss) \\// (ys:yss) = (xs +| ys) : xss \\// yss
+infixr 7 \\//
+
+-- | Take a tiered product of lists of tiers.
+--
+-- > [t0,t1,t2,...] >< [u0,u1,u2,...] =
+-- > [ t0**u0
+-- > , t0**u1 ++ t1**u0
+-- > , t0**u2 ++ t1**u1 ++ t2**u0
+-- > , ...       ...       ...       ...
+-- > ]
+-- > where xs ** ys = [(x,y) | x <- xs, y <- ys]
+--
+-- Example:
+--
+-- > [[0],[1],[2],...] >< [[0],[1],[2],...]
+-- > == [  [(0,0)]
+-- >    ,  [(1,0),(0,1)]
+-- >    ,  [(2,0),(1,1),(0,2)]
+-- >    ,  [(3,0),(2,1),(1,2),(0,3)]
+-- >    ...
+-- >    ]
+(><) :: [[a]] -> [[b]] -> [[(a,b)]]
+(><) = productWith (,)
+infixr 8 ><
+
+-- | Take a tiered product of lists of tiers.
+--   'productWith' can be defined by '><', as:
+--
+-- > productWith f xss yss = map (uncurry f) $ xss >< yss
+productWith :: (a->b->c) -> [[a]] -> [[b]] -> [[c]]
+productWith _ _ [] = []
+productWith _ [] _ = []
+productWith f (xs:xss) yss = map (xs **) yss
+                          \/ productWith f xss yss `addWeight` 1
+  where xs ** ys = [x `f` y | x <- xs, y <- ys]
+
+-- | 'Testable' values are functions
+--   of 'Listable' arguments that return boolean values,
+--   e.g.:
+--
+-- * @ Bool @
+-- * @ Listable a => a -> Bool @
+-- * @ Listable a => a -> a -> Bool @
+-- * @ Int -> Bool @
+-- * @ String -> [Int] -> Bool @
+class Testable a where
+  resultiers :: a -> [[([String],Bool)]]
+
+instance Testable Bool where
+  resultiers p = [[([],p)]]
+
+instance (Testable b, Show a, Listable a) => Testable (a->b) where
+  resultiers p = concatMapT resultiersFor tiers
+    where resultiersFor x = mapFst (showsPrec 11 x "":) `mapT` resultiers (p x)
+          mapFst f (x,y) = (f x, y)
+
+-- | List all results of a 'Testable' property.
+-- Each result is a pair of a list of strings and a boolean.
+-- The list of strings is a printable representation of one possible choice of
+-- argument values for the property.  Each boolean paired with such a list
+-- indicates whether the property holds for this choice.  The outer list is
+-- potentially infinite and lazily evaluated.
+results :: Testable a => a -> [([String],Bool)]
+results = concat . resultiers
+
+-- | Lists all counter-examples for a number of tests to a property,
+counterExamples :: Testable a => Int -> a -> [[String]]
+counterExamples n = map fst . filter (not . snd) . take n . results
+
+-- | Up to a number of tests to a property,
+--   returns 'Just' the first counter-example
+--   or 'Nothing' if there is none.
+--
+-- > counterExample 100 $ \xs -> [] `union` xs == (xs::[Int])
+-- > -- > Just ["[0,0]"]
+counterExample :: Testable a => Int -> a -> Maybe [String]
+counterExample n = listToMaybe . counterExamples n
+
+-- | Lists all witnesses up to a number of tests to a property,
+witnesses :: Testable a => Int -> a -> [[String]]
+witnesses n = map fst . filter snd . take n . results
+
+-- | Up to a number of tests to a property,
+--   returns 'Just' the first witness
+--   or 'Nothing' if there is none.
+witness :: Testable a => Int -> a -> Maybe [String]
+witness n = listToMaybe . witnesses n
+
+-- | Does a property __hold__ up to a number of test values?
+--
+-- > holds 1000 $ \xs -> length (sort xs) == length xs
+holds :: Testable a => Int -> a -> Bool
+holds n = and . take n . map snd . results
+
+-- | Does a property __fail__ for a number of test values?
+--
+-- > fails 1000 $ \xs -> xs ++ ys == ys ++ xs
+fails :: Testable a => Int -> a -> Bool
+fails n = not . holds n
+
+-- | There __exists__ an assignment of values that satisfies a property
+--   up to a number of test values?
+--
+-- > exists 1000 $ \x -> x > 10
+exists :: Testable a => Int -> a -> Bool
+exists n = or . take n . map snd . results
+
+uncurry3 :: (a->b->c->d) -> (a,b,c) -> d
+uncurry3 f (x,y,z) = f x y z
+
+uncurry4 :: (a->b->c->d->e) -> (a,b,c,d) -> e
+uncurry4 f (x,y,z,w) = f x y z w
+
+uncurry5 :: (a->b->c->d->e->f) -> (a,b,c,d,e) -> f
+uncurry5 f (x,y,z,w,v) = f x y z w v
+
+-- | Boolean implication operator.  Useful for defining conditional properties:
+--
+-- > prop_something x y = condition x y ==> something x y
+(==>) :: Bool -> Bool -> Bool
+False ==> _ = True
+True  ==> p = p
+infixr 0 ==>
diff --git a/src/Test/LeanCheck/Derive.hs b/src/Test/LeanCheck/Derive.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Derive.hs
@@ -0,0 +1,158 @@
+{-# LANGUAGE TemplateHaskell, CPP #-}
+-- Experimental module for deriving Listable instances
+--
+-- Needs GHC and Template Haskell (tested on GHC 7.4, 7.6, 7.8 and 7.10)
+module Test.LeanCheck.Derive
+  ( deriveListable
+  )
+where
+
+import Language.Haskell.TH
+import Test.LeanCheck.Basic
+import Control.Monad (unless, liftM, liftM2)
+
+#if __GLASGOW_HASKELL__ < 706
+-- reportWarning was only introduced in GHC 7.6 / TH 2.8
+reportWarning :: String -> Q ()
+reportWarning = report False
+#endif
+
+-- | Derives a Listable instance for a given type 'Name', e.g.:
+--
+-- > data Stack a = Stack a (Stack a) | Empty
+-- > deriveListable ''Stack
+--
+-- Needs @TemplateHaskell@ extension.
+deriveListable :: Name -> DecsQ
+deriveListable t = do
+  is <- t `isInstanceOf` ''Listable
+  if is
+    then do reportWarning $ "Instance Listable "
+                         ++ show t
+                         ++ " already exists, skipping derivation"
+            return []
+    else do cd <- canDeriveListable t
+            unless cd (fail $ "Unable to derive Listable "
+                           ++ show t)
+            reallyDeriveListable t
+
+-- | Checks whether it is possible to derive a Listable instance.
+--
+-- For example, it is not possible if there is no Listable instance for a
+-- type in one of the constructors.
+canDeriveListable :: Name -> Q Bool
+canDeriveListable t = return True -- TODO: Check instances for type-cons args
+
+-- TODO: Somehow check if the enumeration has repetitions, then warn the user.
+reallyDeriveListable :: Name -> DecsQ
+reallyDeriveListable t = do
+  (nt,vs) <- normalizeType t
+#if __GLASGOW_HASKELL__ >= 710
+  cxt <- sequence [[t| Listable $(return v) |] | v <- vs]
+#else
+  cxt <- sequence [classP ''Listable [return v] | v <- vs]
+#endif
+#if __GLASGOW_HASKELL__ >= 708
+  cxt |=>| [d| instance Listable $(return nt)
+                 where tiers = $(conse =<< typeCons t) |]
+#else
+  tiersE <- conse =<< typeCons t
+  return [ InstanceD
+             cxt
+             (AppT (ConT ''Listable) nt)
+             [ValD (VarP 'tiers) (NormalB tiersE) []]
+         ]
+#endif
+  where cone n arity = do
+          (Just consN) <- lookupValueName $ "cons" ++ show arity
+          [| $(varE consN) $(conE n) |]
+        conse = foldr1 (\e1 e2 -> [| $e1 \/ $e2 |]) . map (uncurry cone)
+
+
+-- * Template haskell utilities
+
+-- Normalizes a type by applying it to necessary type variables, making it
+-- accept "zero" parameters.  The normalized type is tupled with a list of
+-- necessary type variables.
+--
+-- Suppose:
+--
+-- > data DT a b c ... = ...
+--
+-- Then, in pseudo-TH:
+--
+-- > normalizeType [t|DT|] == Q (DT a b c ..., [a, b, c, ...])
+normalizeType :: Name -> Q (Type, [Type])
+normalizeType t = do
+  ar <- typeArity t
+  vs <- newVarTs ar
+  return (foldl AppT (ConT t) vs, vs)
+  where
+    newNames :: [String] -> Q [Name]
+    newNames = mapM newName
+    newVarTs :: Int -> Q [Type]
+    newVarTs n = liftM (map VarT)
+               $ newNames (take n . map (:[]) $ cycle ['a'..'z'])
+
+-- Normalizes a type by applying it to units (`()`) while possible.
+--
+-- > normalizeTypeUnits ''Int    === [t| Int |]
+-- > normalizeTypeUnits ''Maybe  === [t| Maybe () |]
+-- > normalizeTypeUnits ''Either === [t| Either () () |]
+normalizeTypeUnits :: Name -> Q Type
+normalizeTypeUnits t = do
+  ar <- typeArity t
+  return (foldl AppT (ConT t) (replicate ar (TupleT 0)))
+
+-- Given a type name and a class name,
+-- returns whether the type is an instance of that class.
+isInstanceOf :: Name -> Name -> Q Bool
+isInstanceOf tn cl = do
+  ty <- normalizeTypeUnits tn
+  isInstance cl [ty]
+
+-- | Given a type name, return the number of arguments taken by that type.
+-- Examples in partially broken TH:
+--
+-- > arity ''Int        === Q 0
+-- > arity ''Int->Int   === Q 0
+-- > arity ''Maybe      === Q 1
+-- > arity ''Either     === Q 2
+-- > arity ''Int->      === Q 1
+--
+-- This works for Data's and Newtype's and it is useful when generating
+-- typeclass instances.
+typeArity :: Name -> Q Int
+typeArity t = do
+  ti <- reify t
+  return . length $ case ti of
+    TyConI (DataD    _ _ ks _ _) -> ks
+    TyConI (NewtypeD _ _ ks _ _) -> ks
+    _                            -> error $ "error (arity): symbol "
+                                         ++ show t
+                                         ++ " is not a newtype or data"
+
+-- Given a type name, returns a list of its type constructor names tupled with
+-- the number of arguments they take.
+typeCons :: Name -> Q [(Name,Int)]
+typeCons t = do
+  ti <- reify t
+  return . map simplify $ case ti of
+    TyConI (DataD    _ _ _ cs _) -> cs
+    TyConI (NewtypeD _ _ _ c  _) -> [c]
+    _ -> error $ "error (typeConstructors): symbol "
+              ++ show t
+              ++ " is neither newtype nor data"
+  where simplify (NormalC n ts)  = (n,length ts)
+        simplify (RecC    n ts)  = (n,length ts)
+        simplify (InfixC  _ n _) = (n,2)
+
+-- Append to instance contexts in a declaration.
+--
+-- > sequence [[|Eq b|],[|Eq c|]] |=>| [t|instance Eq a => Cl (Ty a) where f=g|]
+-- > == [t| instance (Eq a, Eq b, Eq c) => Cl (Ty a) where f = g |]
+(|=>|) :: Cxt -> DecsQ -> DecsQ
+c |=>| qds = do ds <- qds
+                return $ map (`ac` c) ds
+  where ac (InstanceD c ts ds) c' = InstanceD (c++c') ts ds
+        ac d                   _  = d
diff --git a/src/Test/LeanCheck/Error.hs b/src/Test/LeanCheck/Error.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Error.hs
@@ -0,0 +1,118 @@
+-- | A simple property-based testing library based on
+--   enumeration of values via lists of lists.
+--
+-- This module re-exports Test.LeanCheck but some test functions have been
+-- specialized to catch errors (see the explicit export list below).
+--
+-- This module is unsafe, it uses `unsafePerformIO` to catch errors.
+{-# LANGUAGE CPP #-}
+module Test.LeanCheck.Error
+  ( holds
+  , fails
+  , exists
+  , counterExample
+  , counterExamples
+  , witness
+  , witnesses
+  , results
+
+  , errorToNothing
+  , errorToFalse
+  , errorToTrue
+  , anyErrorToNothing
+
+  , module Test.LeanCheck
+  )
+where
+
+#if __GLASGOW_HASKELL__ <= 704
+import Prelude hiding (catch)
+#endif
+
+import Test.LeanCheck hiding
+  ( holds
+  , fails
+  , exists
+  , counterExample
+  , counterExamples
+  , witness
+  , witnesses
+  , results
+  )
+
+import qualified Test.LeanCheck as C
+  ( holds
+  , fails
+  , results
+  )
+
+import Control.Monad (liftM)
+import System.IO.Unsafe (unsafePerformIO)
+import Data.Maybe (listToMaybe)
+import Control.Exception ( Exception
+                         , SomeException
+                         , ArithException
+                         , ArrayException
+                         , ErrorCall
+                         , PatternMatchFail
+                         , catch
+                         , catches
+                         , Handler (Handler)
+                         , evaluate
+                         )
+
+-- | Takes a value and a function.  Ignores the value.  Binds the argument of
+--   the function to the type of the value.
+bindArgumentType :: a -> (a -> b) -> a -> b
+bindArgumentType _ f = f
+
+-- | Transforms a value into 'Just' that value or 'Nothing' on some errors:
+--
+--   * ArithException
+--   * ArrayException
+--   * ErrorCall
+--   * PatternMatchFail
+errorToNothing :: a -> Maybe a
+errorToNothing x = unsafePerformIO $
+  (Just `liftM` evaluate x) `catches` map ($ return Nothing)
+                                      [ hf (undefined :: ArithException)
+                                      , hf (undefined :: ArrayException)
+                                      , hf (undefined :: ErrorCall)
+                                      , hf (undefined :: PatternMatchFail)
+                                      ]
+  where hf :: Exception e => e -> IO a -> Handler a -- handlerFor
+        hf e h = Handler $ bindArgumentType e (\_ -> h)
+
+-- | Transforms a value into 'Just' that value or 'Nothing' on error.
+anyErrorToNothing :: a -> Maybe a
+anyErrorToNothing x = unsafePerformIO $
+  (Just `liftM` evaluate x) `catch` \e -> do let _ = e :: SomeException
+                                             return Nothing
+
+errorToFalse :: Bool -> Bool
+errorToFalse p = case errorToNothing p of
+                   Just p' -> p
+                   Nothing -> False
+
+errorToTrue :: Bool -> Bool
+errorToTrue p = case errorToNothing p of
+                  Just p' -> p
+                  Nothing -> True
+
+
+holds,fails,exists :: Testable a => Int -> a -> Bool
+holds n = errorToFalse . C.holds n
+fails n = errorToTrue  . C.fails n
+exists n = or . take n . map snd . results
+
+counterExample,witness :: Testable a => Int -> a -> Maybe [String]
+counterExample n = listToMaybe . counterExamples n
+witness        n = listToMaybe . witnesses n
+
+counterExamples,witnesses :: Testable a => Int -> a -> [[String]]
+counterExamples n = map fst . filter (not . snd) . take n . results
+witnesses       n = map fst . filter snd         . take n . results
+
+results :: Testable a => a -> [([String],Bool)]
+results = map (mapSnd errorToFalse) . C.results
+  where mapSnd f (x,y) = (x,f y)
diff --git a/src/Test/LeanCheck/Function.hs b/src/Test/LeanCheck/Function.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Function.hs
@@ -0,0 +1,3 @@
+module Test.LeanCheck.Function () where
+import Test.LeanCheck.Function.ListsOfPairs ()
+import Test.LeanCheck.Function.Show ()
diff --git a/src/Test/LeanCheck/Function/CoListable.hs b/src/Test/LeanCheck/Function/CoListable.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Function/CoListable.hs
@@ -0,0 +1,64 @@
+-- | Function enumeration via CoListable typeclass
+--   This currently just a sketch.
+module Test.LeanCheck.Function.CoListable
+where
+
+
+import Test.LeanCheck
+import Data.Maybe (fromMaybe)
+
+
+(\+:/) :: [[a]] -> [[a]] -> [[a]]
+xss \+:/ yss = xss \/ ([]:yss)
+infixr 9 \+:/
+
+
+class CoListable a where
+  coListing :: [[b]] -> [[a -> b]]
+
+
+instance CoListable () where
+  coListing rs = mapT (\r  () -> r) rs
+
+
+instance CoListable Bool where
+  coListing rs = productWith (\r1 r2  b -> if b then r1 else r2) rs rs
+
+
+instance CoListable a => CoListable (Maybe a) where
+  coListing rs = productWith (\z f  m -> case m of Nothing -> z
+                                                   Just x  -> f x) rs (coListing rs)
+
+
+instance (CoListable a, CoListable b) => CoListable (Either a b) where
+  coListing rs = productWith (\f g  e -> case e of Left x  -> f x
+                                                   Right x -> g x) (coListing rs) (coListing rs)
+
+
+instance (CoListable a) => CoListable [a] where
+  coListing rss = mapT const rss
+             \+:/ productWith (\y f  xs -> case xs of []      -> y
+                                                      (x:xs') -> f x xs') rss (coListing (coListing rss))
+
+
+instance CoListable Int where
+  coListing rss = mapT const rss
+             \+:/ product3With (\f g z  i -> if i > 0 then f (i-1)
+                                        else if i < 0 then g (i+1)
+                                             else z) (coListing rss) (coListing rss) rss
+
+
+alts0 :: [[a]] -> [[a]]
+alts0 = id
+
+alts1 :: CoListable a => [[b]] -> [[a->b]]
+alts1 bs = coListing bs
+
+alts2 :: (CoListable a, CoListable b) => [[c]] -> [[a->b->c]]
+alts2 cs = coListing (coListing cs)
+
+alts3 :: (CoListable a, CoListable b, CoListable c) => [[d]] -> [[a->b->c->d]]
+alts3 ds = coListing (coListing (coListing ds))
+
+fListing :: (CoListable a, Listable b) => [[a->b]]
+fListing = coListing tiers
diff --git a/src/Test/LeanCheck/Function/ListsOfPairs.hs b/src/Test/LeanCheck/Function/ListsOfPairs.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Function/ListsOfPairs.hs
@@ -0,0 +1,62 @@
+-- | Function enumeration via lists of pairs.
+module Test.LeanCheck.Function.ListsOfPairs
+  ( functionPairs
+  , associations
+  , pairsToFunction
+  , defaultFunPairsToFunction
+  )
+where
+
+import Test.LeanCheck
+import Test.LeanCheck.Tiers
+import Data.Maybe (fromMaybe)
+
+instance (Eq a, Listable a, Listable b) => Listable (a -> b) where
+  tiers = mapT (uncurry $ flip defaultPairsToFunction)
+        $ functions list tiers
+
+
+functions :: [[a]] -> [[b]] -> [[([(a,b)],b)]]
+functions xss yss =
+  concatMapT
+    (\(r,yss) -> mapT (\ps -> (ps,r)) $ functionPairs xss yss)
+    (choices yss)
+
+
+-- | Given a list of domain values, and tiers of codomain values,
+-- return tiers of lists of ordered pairs of domain and codomain values.
+--
+-- Technically: tiers of left-total functional relations.
+associations :: [a] -> [[b]] -> [[ [(a,b)] ]]
+associations xs sbs = zip xs `mapT` products (const sbs `map` xs)
+
+-- | Given tiers of input values and tiers of output values,
+-- return tiers with all possible lists of input-output pairs.
+-- Those represent functional relations.
+functionPairs :: [[a]] -> [[b]] -> [[[(a,b)]]]
+functionPairs xss yss = concatMapT (`associations` yss)
+                                   (strictlyAscendingListsOf xss)
+
+-- | Returns a function given by a list of input-output pairs.
+-- The result is wrapped in a maybe value.
+-- The output for bound inputs is 'Just' a value.
+-- The output for unbound inputs is 'Nothing'.
+pairsToMaybeFunction :: Eq a => [(a,b)] -> a -> Maybe b
+pairsToMaybeFunction []          _ = Nothing
+pairsToMaybeFunction ((a',r):bs) a | a == a'   = Just r
+                                   | otherwise = pairsToMaybeFunction bs a
+
+-- | Returns a partial function given by a list of input-output pairs.
+--
+-- NOTE: This function *will* return undefined values for unbound inputs.
+pairsToFunction :: Eq a => [(a,b)] -> a -> b
+pairsToFunction bs a = fromMaybe undefined (pairsToMaybeFunction bs a)
+
+
+-- | Returns a function given by a list of input-output pairs and a default value.
+defaultPairsToFunction :: Eq a => b -> [(a,b)] -> a -> b
+defaultPairsToFunction r bs a = fromMaybe r (pairsToMaybeFunction bs a)
+
+
+defaultFunPairsToFunction :: Eq a => (a -> b) -> [(a,b)] -> a -> b
+defaultFunPairsToFunction f bs a = fromMaybe (f a) (pairsToMaybeFunction bs a)
diff --git a/src/Test/LeanCheck/Function/Periodic.hs b/src/Test/LeanCheck/Function/Periodic.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Function/Periodic.hs
@@ -0,0 +1,46 @@
+-- | Periodic function enumeration.
+--   This is just a sketch.
+module Test.LeanCheck.Function.Periodic
+where
+
+
+import Test.LeanCheck
+import Data.List (inits)
+
+
+instance (Eq a, Eq b, Listable a, Listable b) => Listable (a -> b) where
+  tiers = mapT pairsToFunction $ functions list tiers
+
+functions :: Eq b => [a] -> [[b]] -> [[[(a,b)]]]
+functions xs yss = mapT (zip xs . cycle) $ lsPeriodsOfLimit xs yss
+
+functionsz :: Eq b => [[a]] -> [[b]] -> [[[(a,b)]]]
+functionsz xss = functions (concat xss)
+
+
+lsPeriodsOf :: Eq a => [[a]] -> [[[a]]]
+lsPeriodsOf xss = map (filter isPeriod) (listsOf xss)
+
+lsPeriodsOfLimit :: Eq a => [b] -> [[a]] -> [[[a]]]
+lsPeriodsOfLimit ys xss = map (filter isPeriod) (tiersOfLimit ys xss)
+
+
+isPeriod :: Eq a => [a] -> Bool
+isPeriod [] = False
+isPeriod [x] = True
+isPeriod xs = not $ any (`isPeriodOf` xs) $ (tail . init . inits) xs
+
+isPeriodOf :: Eq a => [a] -> [a] -> Bool
+xs `isPeriodOf` ys = length ys `mod` length xs == 0
+                  && and (zipWith (==) (cycle xs) ys)
+
+
+tiersOfLimit :: [b] -> [[a]] -> [[[a]]]
+tiersOfLimit     [] xss = [[[]]]
+tiersOfLimit (_:ys) xss = [[[]]] ++ productWith (:) xss (tiersOfLimit ys xss)
+
+
+pairsToFunction :: Eq a => [(a,b)] -> (a -> b)
+pairsToFunction ((x,y):ps) x' =  if x' == x
+                                   then y
+                                   else pairsToFunction ps x'
diff --git a/src/Test/LeanCheck/Function/Show.hs b/src/Test/LeanCheck/Function/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Function/Show.hs
@@ -0,0 +1,10 @@
+-- | A 'Show' instance for functions.
+module Test.LeanCheck.Function.Show () where
+
+import Test.LeanCheck.Function.ShowFunction
+
+instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
+  showsPrec 0 = (++) . showFunction 8
+  showsPrec _ = (++) . paren . showFunctionLine 4
+    where paren s = "(" ++ s ++ ")"
+
diff --git a/src/Test/LeanCheck/Function/ShowFunction.hs b/src/Test/LeanCheck/Function/ShowFunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Function/ShowFunction.hs
@@ -0,0 +1,173 @@
+-- | This module exports the 'ShowFunction' typeclass,
+--   its instances and related functions.
+--
+-- Using this module, it is possible to implement
+-- a Show instance for functions:
+--
+-- > import Test.LeanCheck.ShowFunction
+-- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
+-- >   show = showFunction 8
+--
+-- This shows functions as a case pattern with up to 8 cases.
+--
+-- The module
+-- @Test.LeanCheck.Function.Show@ ('Test.LeanCheck.Function.Show')
+-- exports an instance like the one above.
+module Test.LeanCheck.Function.ShowFunction
+  ( showFunction
+  , showFunctionLine
+  , Binding
+  , bindings
+  , ShowFunction (..)
+  , tBindingsShow
+  -- * Re-exports
+  , Listable
+  )
+where
+
+import Test.LeanCheck.Core
+import Test.LeanCheck.Error (errorToNothing)
+import Data.List
+import Data.Maybe
+
+-- | A functional binding in a showable format.
+type Binding = ([String], Maybe String)
+
+-- | 'ShowFunction' values are those for which
+--   we can return a list of functional bindings.
+--
+-- As a user, you probably want 'showFunction' and 'showFunctionLine'.
+--
+-- Non functional instances should be defined by:
+--
+-- > instance ShowFunction Ty where tBindings = tBindingsShow
+class ShowFunction a where
+  tBindings :: a -> [[Binding]]
+
+-- | Given a 'ShowFunction' value, return a list of bindings
+--   for printing.  Examples:
+--
+-- > bindings True == [([],True)]
+-- > bindings (id::Int) == [(["0"],"0"), (["1"],"1"), (["-1"],"-1"), ...
+-- > bindings (&&) == [ (["False","False"], "False")
+-- >                  , (["False","True"], "False")
+-- >                  , (["True","False"], "False")
+-- >                  , (["True","True"], "True")
+-- >                  ]
+bindings :: ShowFunction a => a -> [Binding]
+bindings = concat . tBindings
+
+
+-- instances for (algebraic/numeric) data types --
+-- | A default implementation of tBindings for already 'Show'-able types.
+tBindingsShow :: Show a => a -> [[Binding]]
+tBindingsShow x = [[([],errorToNothing $ show x)]]
+
+instance ShowFunction ()   where tBindings = tBindingsShow
+instance ShowFunction Bool where tBindings = tBindingsShow
+instance ShowFunction Int  where tBindings = tBindingsShow
+instance ShowFunction Char where tBindings = tBindingsShow
+instance Show a => ShowFunction [a]       where tBindings = tBindingsShow
+instance Show a => ShowFunction (Maybe a) where tBindings = tBindingsShow
+instance (Show a, Show b) => ShowFunction (a,b) where tBindings = tBindingsShow
+
+
+-- instance for functional value type --
+instance (Show a, Listable a, ShowFunction b) => ShowFunction (a->b) where
+  tBindings f = concatMapT tBindingsFor tiers
+    where tBindingsFor x = mapFst (show x:) `mapT` tBindings (f x)
+          mapFst f (x,y) = (f x, y)
+
+paren :: String -> String
+paren s = "(" ++ s ++ ")"
+
+varnamesFor :: ShowFunction a => a -> [String]
+varnamesFor = zipWith const varnames . fst . head . bindings
+  where varnames = ["x","y","z","w"] ++ map (++"'") varnames
+
+showTuple :: [String] -> String
+showTuple [x] = x
+showTuple xs  = paren $ intercalate "," xs
+
+showNBindingsOf :: ShowFunction a => Int -> Int -> a -> [String]
+showNBindingsOf m n f = take n bs
+                     ++ ["..." | length bs' >= m || length bs > n]
+  where bs' = take m $ bindings f
+        bs = [ showTuple as ++ " -> " ++ r
+             | (as, Just r) <- bs' ]
+
+isValue :: ShowFunction a => a -> Bool
+isValue f = case bindings f of
+              [([],_)] -> True
+              _        -> False
+
+showValueOf :: ShowFunction a => a -> String
+showValueOf x = case snd . head . bindings $ x of
+                  Nothing -> "undefined"
+                  Just x' -> x'
+
+-- | Given a number of patterns to show, shows a 'ShowFunction' value.
+--
+-- > showFunction undefined True == "True"
+-- > showFunction 3 (id::Int) == "\\x -> case x of\n\
+-- >                              \        0 -> 0\n\
+-- >                              \        1 -> 1\n\
+-- >                              \        -1 -> -1\n\
+-- >                              \        ...\n"
+-- > showFunction 4 (&&) == "\\x y -> case (x,y) of\n\
+-- >                         \          (False,False) -> False\n\
+-- >                         \          (False,True) -> False\n\
+-- >                         \          (True,False) -> False\n\
+-- >                         \          (True,True) -> True\n"
+--
+-- This can be used as an implementation of show for functions:
+--
+-- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
+-- >   show = showFunction 8
+showFunction :: ShowFunction a => Int -> a -> String
+showFunction n = showFunctionL False (n*n+1) n
+
+-- | Same as showFunction, but has no line breaks.
+--
+-- > showFunction 2 (id::Int) == "\\x -> case x of 0 -> 0; 1 -> 1; ..."
+showFunctionLine :: ShowFunction a => Int -> a -> String
+showFunctionLine n = showFunctionL True (n*n+1) n
+
+-- | isUndefined checks if a function is totally undefined.
+-- When it is not possible to check all values, it returns false
+isUndefined :: ShowFunction a => Int -> a -> Bool
+isUndefined m f = length bs < m && all (isNothing . snd) bs
+  where bs = take m $ bindings f
+
+-- The first boolean parameter tells if we are showing
+-- the function on a single line
+showFunctionL :: ShowFunction a => Bool -> Int -> Int -> a -> String
+showFunctionL singleLine m n f | isValue f = showValueOf f
+showFunctionL singleLine m n f | otherwise = lambdaPat ++ caseExp
+  where
+    vs = varnamesFor f
+    lambdaPat = "\\" ++ unwords vs ++ " -> "
+    casePat = "case " ++ showTuple vs ++ " of"
+    bs = showNBindingsOf m n f
+    sep | singleLine = " "
+        | otherwise = "\n"
+    cases | singleLine = intercalate "; " bs
+          | otherwise  = unlines
+                       $ (replicate (length lambdaPat + 2) ' ' ++) `map` bs
+    caseExp = if isUndefined m f
+                then "undefined"
+                else casePat ++ sep ++ cases
+
+-- instances for further tuples --
+instance (Show a, Show b, Show c)
+      => ShowFunction (a,b,c) where tBindings = tBindingsShow
+instance (Show a, Show b, Show c, Show d)
+      => ShowFunction (a,b,c,d) where tBindings = tBindingsShow
+instance (Show a, Show b, Show c, Show d, Show e)
+      => ShowFunction (a,b,c,d,e) where tBindings = tBindingsShow
+instance (Show a, Show b, Show c, Show d, Show e, Show f)
+      => ShowFunction (a,b,c,d,e,f) where tBindings = tBindingsShow
+instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g)
+      => ShowFunction (a,b,c,d,e,f,g) where tBindings = tBindingsShow
+instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g, Show h)
+      => ShowFunction (a,b,c,d,e,f,g,h) where tBindings = tBindingsShow
diff --git a/src/Test/LeanCheck/IO.hs b/src/Test/LeanCheck/IO.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/IO.hs
@@ -0,0 +1,85 @@
+-- | QuickCheck-like interface to LeanCheck
+{-# LANGUAGE CPP #-}
+module Test.LeanCheck.IO
+  ( check
+  , checkFor
+  , checkResult
+  , checkResultFor
+  )
+where
+
+#if __GLASGOW_HASKELL__ <= 704
+import Prelude hiding (catch)
+#endif
+
+import Test.LeanCheck.Core
+import Data.Maybe (listToMaybe)
+import Data.List (find)
+import Control.Exception (SomeException, catch, evaluate)
+
+-- | Checks a property printing results on 'stdout'
+--
+-- > > check $ \xs -> sort (sort xs) == sort (xs::[Int])
+-- > +++ OK, passed 200 tests.
+-- > > check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
+-- > *** Failed! Falsifiable (after 4 tests):
+-- > [] [0,0]
+check :: Testable a => a -> IO ()
+check p = checkResult p >> return ()
+
+-- | Check a property for a given number of tests
+--   printing results on 'stdout'
+checkFor :: Testable a => Int -> a -> IO ()
+checkFor n p = checkResultFor n p >> return ()
+
+-- | Check a property
+--   printing results on 'stdout' and
+--   returning 'True' on success.
+--
+-- There is no option to silence this function:
+-- for silence, you should use 'TestLean.Check.holds'.
+checkResult :: Testable a => a -> IO Bool
+checkResult p = checkResultFor 200 p
+
+-- | Check a property for a given number of tests
+--   printing results on 'stdout' and
+--   returning 'True' on success.
+--
+-- There is no option to silence this function:
+-- for silence, you should use 'Test.LeanCheck.holds'.
+checkResultFor :: Testable a => Int -> a -> IO Bool
+checkResultFor n p = do
+  r <- resultIO n p
+  putStrLn . showResult $ r
+  return (isOK r)
+  where isOK (OK _) = True
+        isOK _      = False
+
+data Result = OK        Int
+            | Falsified Int [String]
+            | Exception Int [String] String
+  deriving (Eq, Show)
+
+resultsIO :: Testable a => Int -> a -> IO [Result]
+resultsIO n = sequence . zipWith torio [1..] . take n . results
+  where
+    tor i (_,True) = OK i
+    tor i (as,False) = Falsified i as
+    torio i r@(as,_) = evaluate (tor i r)
+       `catch` \e -> let _ = e :: SomeException
+                     in return (Exception i as (show e))
+
+resultIO :: Testable a => Int -> a -> IO Result
+resultIO n p = do
+  rs <- resultsIO n p
+  return . maybe (last rs) id
+         $ find isFailure rs
+  where isFailure (OK _) = False
+        isFailure _      = True
+
+showResult :: Result -> String
+showResult (OK n)             = "+++ OK, passed " ++ show n ++ " tests."
+showResult (Falsified i ce)   = "*** Failed! Falsifiable (after "
+                             ++ show i ++ " tests):\n" ++ unwords ce
+showResult (Exception i ce e) = "*** Failed! Exception '" ++ e ++ "' (after "
+                             ++ show i ++ " tests):\n" ++ unwords ce
diff --git a/src/Test/LeanCheck/Invariants.hs b/src/Test/LeanCheck/Invariants.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Invariants.hs
@@ -0,0 +1,130 @@
+-- | Some invariants over Test.LeanCheck functions
+--   You should be importing this ONLY to test 'Test/LeanCheck.hs' itself.
+module Test.LeanCheck.Invariants
+  ( tNatPairOrd
+  , tNatTripleOrd
+  , tNatQuadrupleOrd
+  , tNatQuintupleOrd
+  , tNatSixtupleOrd
+  , tNatListOrd
+  , tListsOfNatOrd
+  , tPairEqParams
+  , tTripleEqParams
+  , tProductsIsFilterByLength
+
+  , ordered
+  , orderedBy
+  , strictlyOrdered
+  , strictlyOrderedBy
+  )
+where
+
+import Test.LeanCheck
+import Data.List
+import Data.Ord
+import Test.LeanCheck.Utils.Types (Nat(..))
+
+-- | check if a list is ordered
+ordered :: Ord a => [a] -> Bool
+ordered = orderedBy compare
+-- ordered [] = True
+-- ordered [_] = True
+-- ordered (x:y:xs) = x <= y && ordered (y:xs)
+
+strictlyOrdered :: Ord a => [a] -> Bool
+strictlyOrdered = strictlyOrderedBy compare
+
+-- | check if a list is ordered by a given ordering function
+orderedBy :: (a -> a -> Ordering) -> [a] -> Bool
+orderedBy _ [] = True
+orderedBy _ [_] = True
+orderedBy cmp (x:y:xs) = case x `cmp` y of
+                           GT -> False
+                           _  -> orderedBy cmp (y:xs)
+
+-- | check if a list is strictly ordered by a given ordering function
+strictlyOrderedBy :: (a -> a -> Ordering) -> [a] -> Bool
+strictlyOrderedBy _ [] = True
+strictlyOrderedBy _ [_] = True
+strictlyOrderedBy cmp (x:y:xs) = case x `cmp` y of
+                                   LT -> strictlyOrderedBy cmp (y:xs)
+                                   _  -> False
+
+ifNotEq :: Ordering -> Ordering -> Ordering
+-- Could be implemented as:  ifNotEq = mappend
+ifNotEq EQ p = p
+ifNotEq  o _ = o
+
+thn :: (a->a->Ordering) -> (a->a->Ordering) -> a -> a -> Ordering
+thn cmp1 cmp2 x y = (x `cmp1` y) `ifNotEq` (x `cmp2` y)
+infixr 9 `thn`
+
+
+-- | checks if the first 'n' elements on tiers are ordered by 'cmp'.
+--
+-- > (n `seriesOrderedBy`) comparing (id :: Type)
+tOrderedBy :: Listable a => Int -> (a -> a -> Ordering) -> Bool
+tOrderedBy n cmp = orderedBy cmp $ take n list
+infixr 9 `tOrderedBy`
+
+tStrictlyOrderedBy :: Listable a => Int -> (a -> a -> Ordering) -> Bool
+tStrictlyOrderedBy n cmp = strictlyOrderedBy cmp $ take n list
+infixr 9 `tStrictlyOrderedBy`
+
+tNatPairOrd :: Int -> Bool
+tNatPairOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
+  where sum' (x,y) = x+y :: Nat
+
+tNatTripleOrd :: Int -> Bool
+tNatTripleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
+  where sum' (x,y,z) = x+y+z :: Nat
+
+tNatQuadrupleOrd :: Int -> Bool
+tNatQuadrupleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
+  where sum' (x,y,z,w) = x+y+z+w :: Nat
+
+tNatQuintupleOrd :: Int -> Bool
+tNatQuintupleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
+  where sum' (x,y,z,w,v) = x+y+z+w+v :: Nat
+
+tNatSixtupleOrd :: Int -> Bool
+tNatSixtupleOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
+  where sum' (x,y,z,w,v,u) = x+y+z+w+v+u :: Nat
+
+tNatListOrd :: Int -> Bool
+tNatListOrd n = n `tStrictlyOrderedBy`  comparing sum' `thn` compare
+  where sum' = sum . map (+1) :: [Nat] -> Nat
+
+tListsOfStrictlyOrderedBy :: Int
+                           -> (a -> a -> Ordering)
+                           -> [[a]]
+                           -> Bool
+tListsOfStrictlyOrderedBy n cmp = strictlyOrderedBy cmp . take n . concat
+infixr 9 `tListsOfStrictlyOrderedBy`
+
+tListsOfNatOrd :: Int -> Bool
+tListsOfNatOrd n = tListsOfStrictlyOrderedBy n (comparing sum' `thn` compare) tiers
+  where sum' = sum . map (+1) :: [Nat] -> Nat
+
+tPairEqParams :: Int -> Bool
+tPairEqParams n = ces == srs
+  where
+    ces = map (map read) $ counterExamples n fail
+    srs = map pairToList $ take n list
+    pairToList (x,y) = [x,y :: Nat]
+    fail :: Nat -> Nat -> Bool
+    fail x y = False
+
+tTripleEqParams :: Int -> Bool
+tTripleEqParams n = ces == srs
+  where
+    ces = map (map read) $ counterExamples n fail
+    srs = map tripleToList $ take n list
+    tripleToList (x,y,z) = [x,y,z :: Nat]
+    fail :: Nat -> Nat -> Nat -> Bool
+    fail x y z = False
+
+tProductsIsFilterByLength :: Eq a => [[a]] -> Int -> Int -> Bool
+tProductsIsFilterByLength values m n = concat (take m byProduct) `isPrefixOf` concat byFilter
+  where byProduct = products $ replicate n values
+        byFilter  = ((==n) . length) `filterT` listsOf values
diff --git a/src/Test/LeanCheck/Tiers.hs b/src/Test/LeanCheck/Tiers.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Tiers.hs
@@ -0,0 +1,259 @@
+-- | Utilities functions for manipulating tiers (sized lists of lists)
+module Test.LeanCheck.Tiers
+  (
+  -- * Additional tiers constructors
+    consFromList
+  , consFromAscendingList
+  , consFromStrictlyAscendingList
+  , consFromSet
+  , consFromNoDupList
+
+  -- * Products of tiers
+  , product3With
+  , productMaybeWith
+
+  -- * Tiers of lists
+  , listsOf
+  , ascendingListsOf
+  , strictlyAscendingListsOf
+  , setsOf
+  , noDupListsOf
+  , products
+  , listsOfLength
+
+  , deleteT
+  , normalizeT
+
+  -- * Tiers of choices
+  , choices
+  , ascendingChoices
+  , strictlyAscendingChoices
+  )
+where
+
+import Test.LeanCheck.Basic
+import Data.Maybe (catMaybes)
+
+-- | Given a constructor that takes a list,
+--   return tiers of applications of this constructor.
+--
+--   This is equivalent to 'cons1'.
+consFromList :: Listable a => ([a] -> b) -> [[b]]
+consFromList = (`mapT` listsOf tiers)
+
+-- | Given a constructor that takes a list with ascending elements,
+--   return tiers of applications of this constructor.
+--
+-- For example, a 'Bag' represented as a list.
+--
+-- > consFromAscendingList Bag
+consFromAscendingList :: Listable a => ([a] -> b) -> [[b]]
+consFromAscendingList = (`mapT` ascendingListsOf tiers)
+
+-- | Given a constructor that takes a list with ascending elements,
+--   return tiers of applications of this constructor.
+--
+-- For example, a 'Set' represented as a list.
+--
+-- > consFromAscendingList Set
+consFromStrictlyAscendingList :: Listable a => ([a] -> b) -> [[b]]
+consFromStrictlyAscendingList = (`mapT` strictlyAscendingListsOf tiers)
+
+-- | Given a constructor that takes a set of elements (as a list),
+--   return tiers of applications of this constructor.
+--
+-- For example, a 'Set' represented as a list.
+--
+-- > consFromAscendingList Set
+consFromSet :: Listable a => ([a] -> b) -> [[b]]
+consFromSet = (`mapT` setsOf tiers)
+
+-- | Given a constructor that takes a list with no duplicate elements,
+--   return tiers of applications of this constructor.
+consFromNoDupList :: Listable a => ([a] -> b) -> [[b]]
+consFromNoDupList f = mapT f (noDupListsOf tiers)
+
+
+-- | Like 'productWith', but over 3 lists of tiers.
+product3With :: (a->b->c->d) -> [[a]] -> [[b]] -> [[c]] -> [[d]]
+product3With f xss yss zss = productWith ($) (productWith f xss yss) zss
+
+-- | Take the product of lists of tiers
+--   by a function returning a 'Maybe' value
+--   discarding 'Nothing' values.
+productMaybeWith :: (a->b->Maybe c) -> [[a]] -> [[b]] -> [[c]]
+productMaybeWith _ _ [] = []
+productMaybeWith _ [] _ = []
+productMaybeWith f (xs:xss) yss = map (xs **) yss
+                               \/ productMaybeWith f xss yss `addWeight` 1
+  where xs ** ys = catMaybes [ f x y | x <- xs, y <- ys ]
+
+
+-- | Given tiers of values, returns tiers of lists of those values
+--
+-- > listsOf [[]] == [[[]]]
+--
+-- > listsOf [[x]] == [ [[]]
+-- >                  , [[x]]
+-- >                  , [[x,x]]
+-- >                  , [[x,x,x]]
+-- >                  , ...
+-- >                  ]
+--
+-- > listsOf [[x],[y]] == [ [[]]
+-- >                      , [[x]]
+-- >                      , [[x,x],[y]]
+-- >                      , [[x,x,x],[x,y],[y,x]]
+-- >                      , ...
+-- >                      ]
+listsOf :: [[a]] -> [[[a]]]
+listsOf xss = cons0 []
+           \/ productWith (:) xss (listsOf xss) `addWeight` 1
+
+-- | Generates several lists of the same size.
+--
+-- > products [ xss, yss, zss ] ==
+--
+-- Tiers of all lists combining elements of tiers: xss, yss and zss
+products :: [ [[a]] ] -> [[ [a] ]]
+products = foldr (productWith (:)) [[[]]]
+
+-- | Delete the first occurence of an element in a tier.
+--
+-- For tiers without repetitions, the following holds:
+--
+-- > deleteT x = normalizeT . (`suchThat` (/= x))
+deleteT :: Eq a => a -> [[a]] -> [[a]]
+deleteT _ [] = []
+deleteT y ([]:xss) = [] : deleteT y xss
+deleteT y [[x]]        | x == y    = []
+deleteT y ((x:xs):xss) | x == y    = xs:xss
+                       | otherwise = [[x]] \/ deleteT y (xs:xss)
+
+-- | Normalizes tiers by removing an empty tier from the end of a list of
+--   tiers.
+--
+-- > normalizeT [xs0,xs1,...,xsN,[]] = [xs0,xs1,...,xsN]
+--
+--   Note this will only remove a single empty tier:
+--
+-- > normalizeT [xs0,xs1,...,xsN,[],[]] = [xs0,xs1,...,xsN,[]]
+normalizeT :: [[a]] -> [[a]]
+normalizeT [] = []
+normalizeT [[]] = []
+normalizeT (xs:xss) = xs:normalizeT xss
+
+-- | Given tiers of values, returns tiers of lists with no repeated elements.
+--
+-- > noDupListsOf [[0],[1],[2],...] ==
+-- >   [ [[]]
+-- >   , [[0]]
+-- >   , [[1]]
+-- >   , [[0,1],[1,0],[2]]
+-- >   , [[0,2],[2,0],[3]]
+-- >   , ...
+-- >   ]
+noDupListsOf :: [[a]] -> [[[a]]]
+noDupListsOf =
+  ([[]]:) . concatT . choicesWith (\x xss -> mapT (x:) (noDupListsOf xss))
+
+-- | Lists tiers of all choices of values from tiers.
+-- Choices are pairs of values and tiers excluding that value.
+--
+-- > choices [[False,True]] == [[(False,[[True]]),(True,[[False]])]]
+-- > choices [[1],[2],[3]]
+-- >   == [ [(1,[[],[2],[3]])]
+-- >      , [(2,[[1],[],[3]])]
+-- >      , [(3,[[1],[2],[]])] ]
+--
+-- Each choice is sized by the extracted element.
+choices :: [[a]] -> [[(a,[[a]])]]
+choices = choicesWith (,)
+
+-- | Like 'choices', but allows a custom function.
+choicesWith :: (a -> [[a]] -> b) -> [[a]] -> [[b]]
+choicesWith f []           = []
+choicesWith f [[]]         = []
+choicesWith f ([]:xss)     = [] : choicesWith (\y yss -> f y ([]:yss)) xss
+choicesWith f ((x:xs):xss) = [[f x (xs:xss)]]
+                          \/ choicesWith (\y (ys:yss) -> f y ((x:ys):yss)) (xs:xss)
+
+-- | Given tiers of values,
+--   returns tiers of lists of elements in ascending order
+--                               (from tiered enumeration).
+--
+ascendingListsOf :: [[a]] -> [[[a]]]
+ascendingListsOf =
+  ([[]]:) . concatT . ascendingChoicesWith (\x xss -> mapT (x:) (ascendingListsOf xss))
+
+-- > ascendingChoices [[False,True]] =
+-- >   [ [(False,[[False,True]]), (True,[[True]])]
+-- >   ]
+--
+-- > ascendingChoices [[1],[2],[3],...] =
+-- >   [ [(1,[[1],[2],[3],...])]
+-- >   , [(2,[[ ],[2],[3],...])]
+-- >   , [(3,[[ ],[ ],[3],...])]
+-- >   , ...
+-- >   ]
+ascendingChoices :: [[a]] -> [[(a,[[a]])]]
+ascendingChoices = ascendingChoicesWith (,)
+
+ascendingChoicesWith :: (a -> [[a]] -> b) -> [[a]] -> [[b]]
+ascendingChoicesWith f []           = []
+ascendingChoicesWith f [[]]         = []
+ascendingChoicesWith f ([]:xss)     = [] : ascendingChoicesWith (\y yss -> f y ([]:yss)) xss
+ascendingChoicesWith f ((x:xs):xss) = [[f x ((x:xs):xss)]]
+                                   \/ ascendingChoicesWith f (xs:xss)
+
+-- | Given tiers of values,
+--   returns tiers of lists of elements in strictly ascending order
+--                              (from tiered enumeration).
+--   If you only care about whether elements are in returned lists,
+--   this returns the tiers of all sets of values.
+--
+-- > strictlyAscendingListsOf [[0],[1],[2],...] ==
+-- >   [ [[]]
+-- >   , [[0]]
+-- >   , [[1]]
+-- >   , [[0,1],[2]]
+-- >   , [[0,2],[3]]
+-- >   , [[0,3],[1,2],[4]]
+-- >   , [[0,1,2],[0,4],[1,3],[5]]
+-- >   , ...
+-- >   ]
+strictlyAscendingListsOf :: [[a]] -> [[[a]]]
+strictlyAscendingListsOf =
+  ([[]]:) . concatT .
+  strictlyAscendingChoicesWith
+    (\x xss -> mapT (x:) (strictlyAscendingListsOf xss))
+
+-- | Returns tiers of sets represented as lists of values (no repeated sets).
+--   Shorthand for 'strictlyAscendingListsOf'.
+setsOf :: [[a]] -> [[[a]]]
+setsOf = strictlyAscendingListsOf
+
+-- | Like 'choices', but paired tiers are always strictly ascending (in terms
+--   of enumeration).
+--
+-- > strictlyAscendingChoices [[False,True]] == [[(False,[[True]]),(True,[[]])]]
+-- > strictlyAscendingChoices [[1],[2],[3]]
+-- >   == [ [(1,[[],[2],[3]])]
+-- >      , [(2,[[],[],[3]])]
+-- >      , [(3,[[],[],[]])]
+-- >      ]
+strictlyAscendingChoices :: [[a]] -> [[(a,[[a]])]]
+strictlyAscendingChoices = strictlyAscendingChoicesWith (,)
+
+-- | Like 'strictlyAscendingChoices' but customized by a function.
+strictlyAscendingChoicesWith :: (a -> [[a]] -> b) -> [[a]] -> [[b]]
+strictlyAscendingChoicesWith f []           = []
+strictlyAscendingChoicesWith f [[]]         = []
+strictlyAscendingChoicesWith f ([]:xss)     = [] : strictlyAscendingChoicesWith (\y yss -> f y ([]:yss)) xss
+strictlyAscendingChoicesWith f ((x:xs):xss) = [[f x (xs:xss)]]
+                                           \/ strictlyAscendingChoicesWith f (xs:xss)
+
+
+-- | Given tiers, returns tiers of lists of a given length.
+listsOfLength :: Int -> [[a]] -> [[[a]]]
+listsOfLength n xss = products (replicate n xss)
diff --git a/src/Test/LeanCheck/Utils.hs b/src/Test/LeanCheck/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Utils.hs
@@ -0,0 +1,10 @@
+module Test.LeanCheck.Utils
+  ( module Test.LeanCheck.Utils.Types
+  , module Test.LeanCheck.Utils.Operators
+  , module Test.LeanCheck.Utils.TypeBinding
+  )
+where
+
+import Test.LeanCheck.Utils.Types
+import Test.LeanCheck.Utils.Operators
+import Test.LeanCheck.Utils.TypeBinding
diff --git a/src/Test/LeanCheck/Utils/Operators.hs b/src/Test/LeanCheck/Utils/Operators.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Utils/Operators.hs
@@ -0,0 +1,113 @@
+module Test.LeanCheck.Utils.Operators
+  (
+--  (==>) -- already provided by Test.LeanCheck
+
+  -- * Combining properties
+    (===), (====)
+  , (&&&), (&&&&)
+  , (|||), (||||)
+
+  -- * Properties over functions
+  , commutative
+  , associative
+  , distributive
+  , transitive
+  , idempotent
+  , identity
+  , notIdentity
+
+  -- * Ternary comparison operators
+  , (=$), ($=)
+  , (=|), (|=)
+  )
+where
+
+import Test.LeanCheck ((==>))
+
+combine :: (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
+combine op f g = \x -> f x `op` g x
+
+-- Uneeded, just food for thought
+--combine2 :: (c -> d -> e) -> (a -> b -> c) -> (a -> b -> d) -> (a -> b -> e)
+-- Two possible implementations:
+--combine2 op f g = \x y -> f x y `op` g x y
+--combine2 = combine . combine
+
+(===) :: Eq b => (a -> b) -> (a -> b) -> a -> Bool
+(===) = combine (==)
+infix 4 ===
+
+(====) :: Eq c => (a -> b -> c) -> (a -> b -> c) -> a -> b -> Bool
+(====) = combine (===)
+infix 4 ====
+
+(&&&) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
+(&&&) = combine (&&)
+infix 3 &&&
+
+(&&&&) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
+(&&&&) = combine (&&&)
+infix 3 &&&&
+
+(|||) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
+(|||) = combine (||)
+infix 2 |||
+
+(||||) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
+(||||) = combine (|||)
+infix 2 ||||
+
+commutative :: Eq b => (a -> a -> b) -> a -> a -> Bool
+commutative o = \x y -> x `o` y == y `o` x
+
+associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
+associative o = \x y z -> x `o` (y `o` z) == (x `o` y) `o` z
+
+-- type could be more general: (b -> a -> a) for both operators
+distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
+distributive o o' = \x y z -> x `o` (y `o'` z) == (x `o` y) `o'` (x `o` z)
+
+transitive :: (a -> a -> Bool) -> a -> a -> a -> Bool
+transitive o = \x y z -> x `o` y && y `o` z ==> x `o` z
+
+idempotent :: Eq a => (a -> a) -> a -> Bool
+idempotent f = f . f === f
+
+identity :: Eq a => (a -> a) -> a -> Bool
+identity f = f === id
+
+notIdentity :: Eq a => (a -> a) -> a -> Bool
+notIdentity = (not .) . identity
+
+-- | Equal under.  A ternary operator.
+--
+-- > x =$ f $= y  =  f x = f y
+--
+-- > [1,2,3,4,5] =$  take 2    $= [1,2,4,8,16] -- > True
+-- > [1,2,3,4,5] =$  take 3    $= [1,2,4,8,16] -- > False
+-- >     [1,2,3] =$    sort    $= [3,2,1]      -- > True
+-- >          42 =$ (`mod` 10) $= 16842        -- > True
+-- >          42 =$ (`mod`  9) $= 16842        -- > False
+-- >         'a' =$  isLetter  $= 'b'          -- > True
+-- >         'a' =$  isLetter  $= '1'          -- > False
+(=$) :: Eq b => a -> (a -> b) -> a -> Bool
+(x =$ f) y = f x == f y
+infixl 4 =$
+
+($=) :: (a -> Bool) -> a -> Bool
+($=) = ($)
+infixl 4 $=
+
+-- | Check if two lists are equal for @n@ values.
+--
+-- > xs =| n |= ys  =  take n xs == take n ys
+--
+-- > [1,2,3,4,5] =| 2 |= [1,2,4,8,16] -- > True
+-- > [1,2,3,4,5] =| 3 |= [1,2,4,8,16] -- > False
+(=|) :: Eq a => [a] -> Int -> [a] -> Bool
+xs =| n = xs =$ take n
+infixl 4 =|
+
+(|=) :: (a -> Bool) -> a -> Bool
+(|=) = ($)
+infixl 4 |=
diff --git a/src/Test/LeanCheck/Utils/TypeBinding.hs b/src/Test/LeanCheck/Utils/TypeBinding.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Utils/TypeBinding.hs
@@ -0,0 +1,229 @@
+-- | Infix operators for type binding using dummy first-class values.
+--
+-- Those are useful when property based testing to avoid repetition.
+-- Suppose:
+--
+-- > prop_sortAppend :: Ord a => [a] -> Bool
+-- > prop_sortAppend xs =  sort (xs++ys) == sort (ys++xs)
+--
+-- Then this:
+--
+-- > testResults n =
+-- >   [ holds n (prop_sortAppend :: [Int] -> [Int] -> Bool)
+-- >   , holds n (prop_sortAppend :: [UInt2] -> [UInt2] -> Bool)
+-- >   , holds n (prop_sortAppend :: [Bool] -> [Bool] -> Bool)
+-- >   , holds n (prop_sortAppend :: [Char] -> [Char] -> Bool)
+-- >   , holds n (prop_sortAppend :: [String] -> [String] -> Bool)
+-- >   , holds n (prop_sortAppend :: [()] -> [()] -> Bool)
+-- >   ]
+--
+-- Becomes this:
+--
+-- > testResults n =
+-- >   [ holds n $ prop_sortAppend -:> [int]
+-- >   , holds n $ prop_sortAppend -:> [uint2]
+-- >   , holds n $ prop_sortAppend -:> [bool]
+-- >   , holds n $ prop_sortAppend -:> [char]
+-- >   , holds n $ prop_sortAppend -:> [string]
+-- >   , holds n $ prop_sortAppend -:> [()]
+-- >   ]
+--
+-- Or even:
+--
+-- > testResults n = concat
+-- >   [ for int, for uint2, for bool, for (), for char, for string ]
+-- >   where for a = [ holds n $ prop_sortAppend -:> a ]
+--
+-- This last form is useful when testing multiple properties for multiple
+-- types.
+module Test.LeanCheck.Utils.TypeBinding
+  (
+  -- * Type binding operators
+  --
+  -- | Summary:
+  --
+  -- *                 as type of: '-:'
+  -- *        argument as type of: '-:>'
+  -- *          result as type of: '->:'
+  -- * second argument as type of: '->:>'
+  -- * second  result  as type of: '->>:'
+  -- * third  argument as type of: '->>:>'
+  -- * third   result  as type of: '->>>:'
+    (-:)
+  , (-:>)
+  , (->:)
+  , (->:>)
+  , (->>:)
+  , (->>:>)
+  , (->>>:)
+
+  -- * Dummy (undefined) values
+  -- ** Standard Haskell types
+  , und
+  , (>-)
+  , bool
+  , int, integer
+  , float, double
+  , char, string
+  , mayb, eith
+  -- ** Testing types
+  , nat
+  , int1, uint1
+  , int2, uint2
+  , int3, uint3
+  , int4, uint4
+  )
+where
+
+import Test.LeanCheck.Utils.Types
+
+undefinedOf :: String -> a
+undefinedOf fn = error $ "Test.LeanCheck.TypeBinding." ++ fn
+
+-- | Type restricted version of const
+-- that forces its first argument
+-- to have the same type as the second.
+-- A symnonym to 'asTypeOf':
+--
+-- >  value -: ty  =  value :: Ty
+--
+-- Examples:
+--
+-- >  10 -: int   =  10 :: Int
+-- >  undefined -: 'a' >- 'b'  =  undefined :: Char -> Char
+(-:) :: a -> a -> a
+(-:) = asTypeOf -- const
+infixl 1 -:
+
+-- | Type restricted version of const
+-- that forces the argument of its first argument
+-- to have the same type as the second:
+--
+-- >  f -:> ty  =  f -: ty >- und  =  f :: Ty -> a
+--
+-- Example:
+--
+-- >  abs -:> int   =  abs -: int >- und  =  abs :: Int -> Int
+(-:>) :: (a -> b) -> a -> (a -> b)
+(-:>) = const
+infixl 1 -:>
+
+-- | Type restricted version of const
+-- that forces the result of its first argument
+-- to have the same type as the second.
+--
+-- >  f ->: ty  =  f -: und >- ty  =  f :: a -> Ty
+(->:) :: (a -> b) -> b -> (a -> b)
+(->:) = const
+infixl 1 ->:
+
+-- | Type restricted version of const
+-- that forces the second argument of its first argument
+-- to have the same type as the second.
+--
+-- > f ->:> ty   =  f -: und -> ty -> und  =  f :: a -> Ty -> b
+(->:>) :: (a -> b -> c) -> b -> (a -> b -> c)
+(->:>) = const
+infixl 1 ->:>
+
+-- | Type restricted version of const
+-- that forces the result of the result of its first argument
+-- to have the same type as the second.
+--
+-- > f ->>: ty   =  f -: und -> und -> ty  =  f :: a -> b -> Ty
+(->>:) :: (a -> b -> c) -> c -> (a -> b -> c)
+(->>:) = const
+infixl 1 ->>:
+
+-- | Type restricted version of const
+-- that forces the third argument of its first argument
+-- to have the same type as the second.
+(->>:>) :: (a -> b -> c -> d) -> c -> (a -> b -> c -> d)
+(->>:>) = const
+infixl 1 ->>:>
+
+-- | Type restricted version of const
+-- that forces the result of the result of the result of its first argument
+-- to have the same type as the second.
+(->>>:) :: (a -> b -> c -> d) -> d -> (a -> b -> c -> d)
+(->>>:) = const
+infixl 1 ->>>:
+
+-- | Returns an undefined functional value
+-- that takes an argument of the type of its first argument
+-- and return a value of the type of its second argument.
+--
+-- > ty >- ty  =  (undefined :: Ty -> Ty)
+--
+-- Examples:
+--
+-- > 'a' >- 'b'  =  char >- char  =  (undefined :: Char -> Char)
+-- > int >- bool >- int  =  undefined :: Int -> Bool -> Int
+(>-) :: a -> b -> (a -> b)
+(>-) = undefinedOf "(>-): undefined function -- using dummy value?"
+infixr 9 >-
+
+
+-- Dummy values of standard Haskell types
+
+-- | Shorthand for undefined
+und :: a
+und = undefinedOf "und"
+
+int :: Int
+int = undefinedOf "int"
+
+integer :: Integer
+integer = undefinedOf "integer"
+
+float :: Float
+float = undefinedOf "float"
+
+double :: Double
+double = undefinedOf "double"
+
+bool :: Bool
+bool = undefinedOf "bool"
+
+char :: Char
+char = undefinedOf "char"
+
+string :: String
+string = undefinedOf "string"
+
+-- | It might be better to just use 'Just'
+mayb :: a -> Maybe a
+mayb = undefinedOf "mayb"
+
+eith :: a -> b -> Either a b
+eith = undefinedOf "eith"
+
+
+-- Dummy values of Test.LeanCheck.Types's types:
+
+nat :: Nat
+nat = undefinedOf "nat"
+
+int1 :: Int1
+int1 = undefinedOf "int1"
+
+int2 :: Int2
+int2 = undefinedOf "int2"
+
+int3 :: Int3
+int3 = undefinedOf "int3"
+
+int4 :: Int4
+int4 = undefinedOf "int4"
+
+uint1 :: UInt1
+uint1 = undefinedOf "uint1"
+
+uint2 :: UInt2
+uint2 = undefinedOf "uint2"
+
+uint3 :: UInt3
+uint3 = undefinedOf "uint3"
+
+uint4 :: UInt4
+uint4 = undefinedOf "uint4"
diff --git a/src/Test/LeanCheck/Utils/Types.hs b/src/Test/LeanCheck/Utils/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/LeanCheck/Utils/Types.hs
@@ -0,0 +1,438 @@
+-- | Types to aid in property-based testing.
+module Test.LeanCheck.Utils.Types
+  (
+  -- * Integer types
+  --
+  -- | Small-width integer types to aid in property-based testing.
+  -- Sometimes it is useful to limit the possibilities of enumerated values
+  -- when testing polymorphic functions, these types allow that.
+  --
+  -- The signed integer types @IntN@ are of limited bit width @N@
+  -- bounded by @-2^(N-1)@ to @2^(N-1)-1@.
+  -- The unsigned integer types @WordN@ are of limited bit width @N@
+  -- bounded by @0@ to @2^N-1@.
+  --
+  -- Operations are closed and modulo @2^N@.  e.g.:
+  --
+  -- > maxBound + 1      = minBound
+  -- > read "2"          = -2 :: Int2
+  -- > abs minBound      = minBound
+  -- > negate n          = 2^N - n :: WordN
+    Int1
+  , Int2
+  , Int3
+  , Int4
+  , Word1
+  , Word2
+  , Word3
+  , Word4
+  , Nat
+  , Nat1
+  , Nat2
+  , Nat3
+  , Nat4
+  , Nat5
+  , Nat6
+  , Nat7
+
+  -- * Aliases to word types (deprecated)
+  , UInt1
+  , UInt2
+  , UInt3
+  , UInt4
+  )
+where
+-- TODO: Add Ix and Bits instances
+
+import Test.LeanCheck (Listable(..), listIntegral)
+import Data.Ratio ((%))
+
+narrowU :: Int -> Int -> Int
+narrowU w i = i `mod` 2^w
+
+narrowS :: Int -> Int -> Int
+narrowS w i = let l  = 2^w
+                  i' = i `mod` l
+              in if i' < 2^(w-1)
+                   then i'
+                   else i' - l
+
+mapTuple :: (a -> b) -> (a,a) -> (b,b)
+mapTuple f (x,y) = (f x, f y)
+
+mapFst :: (a -> b) -> (a,c) -> (b,c)
+mapFst f (x,y) = (f x,y)
+
+oNewtype :: (a -> b) -> (b -> a) -> (a -> a -> a) -> (b -> b -> b)
+oNewtype con des o = \x y -> con $ des x `o` des y
+
+fNewtype :: (a -> b) -> (b -> a) -> (a -> a) -> (b -> b)
+fNewtype con des f = con . f . des
+
+otNewtype :: (a -> b) -> (b -> a) -> (a -> a -> (a,a)) -> (b -> b -> (b,b))
+otNewtype con des o = \x y -> mapTuple con $ des x `o` des y
+
+readsPrecNewtype :: Read a => (a -> b) -> Int -> String -> [(b,String)]
+readsPrecNewtype con n = map (mapFst con) . readsPrec n
+
+boundedEnumFrom :: (Ord a,Bounded a,Enum a) => a -> [a]
+boundedEnumFrom x = [x..maxBound]
+
+boundedEnumFromThen :: (Ord a,Bounded a,Enum a) => a -> a -> [a]
+boundedEnumFromThen x y | x > y     = [x,y..minBound]
+                        | otherwise = [x,y..maxBound]
+
+-- | Single-bit signed integers: -1, 0
+newtype Int1 = Int1 { unInt1 :: Int } deriving (Eq, Ord)
+
+-- | Two-bit signed integers: -2, -1, 0, 1
+newtype Int2 = Int2 { unInt2 :: Int } deriving (Eq, Ord)
+
+-- | Three-bit signed integers: -4, -3, -2, -1, 0, 1, 2, 3
+newtype Int3 = Int3 { unInt3 :: Int } deriving (Eq, Ord)
+
+-- | Four-bit signed integers:
+-- -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7
+newtype Int4 = Int4 { unInt4 :: Int } deriving (Eq, Ord)
+
+-- | Single-bit unsigned integer: 0, 1
+newtype Word1 = Word1 { unWord1 :: Int } deriving (Eq, Ord)
+
+-- | Two-bit unsigned integers: 0, 1, 2, 3
+newtype Word2 = Word2 { unWord2 :: Int } deriving (Eq, Ord)
+
+-- | Three-bit unsigned integers: 0, 1, 2, 3, 4, 5, 6, 7
+newtype Word3 = Word3 { unWord3 :: Int } deriving (Eq, Ord)
+
+-- | Four-bit unsigned integers:
+-- 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15
+newtype Word4 = Word4 { unWord4 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers (including 0): 0, 1, 2, 3, 4, 5, 6, 7, ...
+--
+-- Internally, this type is represented as an 'Int'.
+-- So, it is limited by the 'maxBound' of 'Int'.
+newtype Nat = Nat { unNat :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 1: 0
+newtype Nat1 = Nat1 { unNat1 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 2: 0, 1
+newtype Nat2 = Nat2 { unNat2 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 3: 0, 1, 2
+newtype Nat3 = Nat3 { unNat3 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 4: 0, 1, 2, 3
+newtype Nat4 = Nat4 { unNat4 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 5: 0, 1, 2, 3, 4
+newtype Nat5 = Nat5 { unNat5 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 6: 0, 1, 2, 3, 4, 5
+newtype Nat6 = Nat6 { unNat6 :: Int } deriving (Eq, Ord)
+
+-- | Natural numbers modulo 7: 0, 1, 2, 3, 4, 5, 6
+newtype Nat7 = Nat7 { unNat7 :: Int } deriving (Eq, Ord)
+
+int1  :: Int -> Int1;   int1  = Int1  . narrowS 1
+int2  :: Int -> Int2;   int2  = Int2  . narrowS 2
+int3  :: Int -> Int3;   int3  = Int3  . narrowS 3
+int4  :: Int -> Int4;   int4  = Int4  . narrowS 4
+word1 :: Int -> Word1;  word1 = Word1 . narrowU 1
+word2 :: Int -> Word2;  word2 = Word2 . narrowU 2
+word3 :: Int -> Word3;  word3 = Word3 . narrowU 3
+word4 :: Int -> Word4;  word4 = Word4 . narrowU 4
+nat1 :: Int -> Nat1;  nat1 = Nat1 . (`mod` 1)
+nat2 :: Int -> Nat2;  nat2 = Nat2 . (`mod` 2)
+nat3 :: Int -> Nat3;  nat3 = Nat3 . (`mod` 3)
+nat4 :: Int -> Nat4;  nat4 = Nat4 . (`mod` 4)
+nat5 :: Int -> Nat5;  nat5 = Nat5 . (`mod` 5)
+nat6 :: Int -> Nat6;  nat6 = Nat6 . (`mod` 6)
+nat7 :: Int -> Nat7;  nat7 = Nat7 . (`mod` 7)
+
+oInt1  ::(Int->Int->Int)->(Int1->Int1->Int1)   ; oInt1  = oNewtype int1  unInt1
+oInt2  ::(Int->Int->Int)->(Int2->Int2->Int2)   ; oInt2  = oNewtype int2  unInt2
+oInt3  ::(Int->Int->Int)->(Int3->Int3->Int3)   ; oInt3  = oNewtype int3  unInt3
+oInt4  ::(Int->Int->Int)->(Int4->Int4->Int4)   ; oInt4  = oNewtype int4  unInt4
+oWord1 ::(Int->Int->Int)->(Word1->Word1->Word1); oWord1 = oNewtype word1 unWord1
+oWord2 ::(Int->Int->Int)->(Word2->Word2->Word2); oWord2 = oNewtype word2 unWord2
+oWord3 ::(Int->Int->Int)->(Word3->Word3->Word3); oWord3 = oNewtype word3 unWord3
+oWord4 ::(Int->Int->Int)->(Word4->Word4->Word4); oWord4 = oNewtype word4 unWord4
+oNat   ::(Int->Int->Int)->(Nat->Nat->Nat)      ; oNat   = oNewtype Nat   unNat
+oNat1  ::(Int->Int->Int)->(Nat1->Nat1->Nat1)   ; oNat1  = oNewtype nat1  unNat1
+oNat2  ::(Int->Int->Int)->(Nat2->Nat2->Nat2)   ; oNat2  = oNewtype nat2  unNat2
+oNat3  ::(Int->Int->Int)->(Nat3->Nat3->Nat3)   ; oNat3  = oNewtype nat3  unNat3
+oNat4  ::(Int->Int->Int)->(Nat4->Nat4->Nat4)   ; oNat4  = oNewtype nat4  unNat4
+oNat5  ::(Int->Int->Int)->(Nat5->Nat5->Nat5)   ; oNat5  = oNewtype nat5  unNat5
+oNat6  ::(Int->Int->Int)->(Nat6->Nat6->Nat6)   ; oNat6  = oNewtype nat6  unNat6
+oNat7  ::(Int->Int->Int)->(Nat7->Nat7->Nat7)   ; oNat7  = oNewtype nat7  unNat7
+
+fInt1  :: (Int->Int) -> (Int1->Int1)   ; fInt1  = fNewtype int1  unInt1
+fInt2  :: (Int->Int) -> (Int2->Int2)   ; fInt2  = fNewtype int2  unInt2
+fInt3  :: (Int->Int) -> (Int3->Int3)   ; fInt3  = fNewtype int3  unInt3
+fInt4  :: (Int->Int) -> (Int4->Int4)   ; fInt4  = fNewtype int4  unInt4
+fWord1 :: (Int->Int) -> (Word1->Word1) ; fWord1 = fNewtype word1 unWord1
+fWord2 :: (Int->Int) -> (Word2->Word2) ; fWord2 = fNewtype word2 unWord2
+fWord3 :: (Int->Int) -> (Word3->Word3) ; fWord3 = fNewtype word3 unWord3
+fWord4 :: (Int->Int) -> (Word4->Word4) ; fWord4 = fNewtype word4 unWord4
+fNat   :: (Int->Int) -> (Nat->Nat)     ; fNat   = fNewtype Nat   unNat
+fNat1  :: (Int->Int) -> (Nat1->Nat1)   ; fNat1  = fNewtype nat1  unNat1
+fNat2  :: (Int->Int) -> (Nat2->Nat2)   ; fNat2  = fNewtype nat2  unNat2
+fNat3  :: (Int->Int) -> (Nat3->Nat3)   ; fNat3  = fNewtype nat3  unNat3
+fNat4  :: (Int->Int) -> (Nat4->Nat4)   ; fNat4  = fNewtype nat4  unNat4
+fNat5  :: (Int->Int) -> (Nat5->Nat5)   ; fNat5  = fNewtype nat5  unNat5
+fNat6  :: (Int->Int) -> (Nat6->Nat6)   ; fNat6  = fNewtype nat6  unNat6
+fNat7  :: (Int->Int) -> (Nat7->Nat7)   ; fNat7  = fNewtype nat7  unNat7
+
+instance Show Int1 where show = show . unInt1
+instance Show Int2 where show = show . unInt2
+instance Show Int3 where show = show . unInt3
+instance Show Int4 where show = show . unInt4
+instance Show Word1 where show = show . unWord1
+instance Show Word2 where show = show . unWord2
+instance Show Word3 where show = show . unWord3
+instance Show Word4 where show = show . unWord4
+instance Show Nat where show (Nat x) = show x
+instance Show Nat1 where show = show . unNat1
+instance Show Nat2 where show = show . unNat2
+instance Show Nat3 where show = show . unNat3
+instance Show Nat4 where show = show . unNat4
+instance Show Nat5 where show = show . unNat5
+instance Show Nat6 where show = show . unNat6
+instance Show Nat7 where show = show . unNat7
+
+instance Read Int1 where readsPrec = readsPrecNewtype int1
+instance Read Int2 where readsPrec = readsPrecNewtype int2
+instance Read Int3 where readsPrec = readsPrecNewtype int3
+instance Read Int4 where readsPrec = readsPrecNewtype int4
+instance Read Word1 where readsPrec = readsPrecNewtype word1
+instance Read Word2 where readsPrec = readsPrecNewtype word2
+instance Read Word3 where readsPrec = readsPrecNewtype word3
+instance Read Word4 where readsPrec = readsPrecNewtype word4
+instance Read Nat where readsPrec = readsPrecNewtype Nat
+instance Read Nat1 where readsPrec = readsPrecNewtype nat1
+instance Read Nat2 where readsPrec = readsPrecNewtype nat2
+instance Read Nat3 where readsPrec = readsPrecNewtype nat3
+instance Read Nat4 where readsPrec = readsPrecNewtype nat4
+instance Read Nat5 where readsPrec = readsPrecNewtype nat5
+instance Read Nat6 where readsPrec = readsPrecNewtype nat6
+instance Read Nat7 where readsPrec = readsPrecNewtype nat7
+
+
+instance Num Int1 where (+) = oInt1 (+);  abs    = fInt1 abs
+                        (-) = oInt1 (-);  signum = fInt1 signum
+                        (*) = oInt1 (*);  fromInteger = int1 . fromInteger
+
+instance Num Int2 where (+) = oInt2 (+);  abs    = fInt2 abs
+                        (-) = oInt2 (-);  signum = fInt2 signum
+                        (*) = oInt2 (*);  fromInteger = int2 . fromInteger
+
+instance Num Int3 where (+) = oInt3 (+);  abs    = fInt3 abs
+                        (-) = oInt3 (-);  signum = fInt3 signum
+                        (*) = oInt3 (*);  fromInteger = int3 . fromInteger
+
+instance Num Int4 where (+) = oInt4 (+);  abs    = fInt4 abs
+                        (-) = oInt4 (-);  signum = fInt4 signum
+                        (*) = oInt4 (*);  fromInteger = int4 . fromInteger
+
+instance Num Word1 where (+) = oWord1 (+);  abs    = fWord1 abs
+                         (-) = oWord1 (-);  signum = fWord1 signum
+                         (*) = oWord1 (*);  fromInteger = word1 . fromInteger
+
+instance Num Word2 where (+) = oWord2 (+);  abs    = fWord2 abs
+                         (-) = oWord2 (-);  signum = fWord2 signum
+                         (*) = oWord2 (*);  fromInteger = word2 . fromInteger
+
+instance Num Word3 where (+) = oWord3 (+);  abs    = fWord3 abs
+                         (-) = oWord3 (-);  signum = fWord3 signum
+                         (*) = oWord3 (*);  fromInteger = word3 . fromInteger
+
+instance Num Word4 where (+) = oWord4 (+);  abs    = fWord4 abs
+                         (-) = oWord4 (-);  signum = fWord4 signum
+                         (*) = oWord4 (*);  fromInteger = word4 . fromInteger
+
+instance Num Nat where (+) = oNat (+);  abs    = fNat abs
+                       (-) = oNat (-);  signum = fNat signum
+                       (*) = oNat (*);  fromInteger = Nat . fromInteger
+
+instance Num Nat1 where (+) = oNat1 (+);  abs    = fNat1 abs
+                        (-) = oNat1 (-);  signum = fNat1 signum
+                        (*) = oNat1 (*);  fromInteger = nat1 . fromInteger
+
+instance Num Nat2 where (+) = oNat2 (+);  abs    = fNat2 abs
+                        (-) = oNat2 (-);  signum = fNat2 signum
+                        (*) = oNat2 (*);  fromInteger = nat2 . fromInteger
+
+instance Num Nat3 where (+) = oNat3 (+);  abs    = fNat3 abs
+                        (-) = oNat3 (-);  signum = fNat3 signum
+                        (*) = oNat3 (*);  fromInteger = nat3 . fromInteger
+
+instance Num Nat4 where (+) = oNat4 (+);  abs    = fNat4 abs
+                        (-) = oNat4 (-);  signum = fNat4 signum
+                        (*) = oNat4 (*);  fromInteger = nat4 . fromInteger
+
+instance Num Nat5 where (+) = oNat5 (+);  abs    = fNat5 abs
+                        (-) = oNat5 (-);  signum = fNat5 signum
+                        (*) = oNat5 (*);  fromInteger = nat5 . fromInteger
+
+instance Num Nat6 where (+) = oNat6 (+);  abs    = fNat6 abs
+                        (-) = oNat6 (-);  signum = fNat6 signum
+                        (*) = oNat6 (*);  fromInteger = nat6 . fromInteger
+
+instance Num Nat7 where (+) = oNat7 (+);  abs    = fNat7 abs
+                        (-) = oNat7 (-);  signum = fNat7 signum
+                        (*) = oNat7 (*);  fromInteger = nat7 . fromInteger
+
+
+instance Real Int1 where toRational (Int1 x) = fromIntegral x % 1
+instance Real Int2 where toRational (Int2 x) = fromIntegral x % 1
+instance Real Int3 where toRational (Int3 x) = fromIntegral x % 1
+instance Real Int4 where toRational (Int4 x) = fromIntegral x % 1
+instance Real Word1 where toRational (Word1 x) = fromIntegral x % 1
+instance Real Word2 where toRational (Word2 x) = fromIntegral x % 1
+instance Real Word3 where toRational (Word3 x) = fromIntegral x % 1
+instance Real Word4 where toRational (Word4 x) = fromIntegral x % 1
+instance Real Nat where toRational (Nat x) = fromIntegral x % 1
+instance Real Nat1 where toRational (Nat1 x) = fromIntegral x % 1
+instance Real Nat2 where toRational (Nat2 x) = fromIntegral x % 1
+instance Real Nat3 where toRational (Nat3 x) = fromIntegral x % 1
+instance Real Nat4 where toRational (Nat4 x) = fromIntegral x % 1
+instance Real Nat5 where toRational (Nat5 x) = fromIntegral x % 1
+instance Real Nat6 where toRational (Nat6 x) = fromIntegral x % 1
+instance Real Nat7 where toRational (Nat7 x) = fromIntegral x % 1
+
+instance Integral Int1 where quotRem = otNewtype int1 unInt1 quotRem
+                             toInteger = toInteger . unInt1
+
+instance Integral Int2 where quotRem = otNewtype int2 unInt2 quotRem
+                             toInteger = toInteger . unInt2
+
+instance Integral Int3 where quotRem = otNewtype int3 unInt3 quotRem
+                             toInteger = toInteger . unInt3
+
+instance Integral Int4 where quotRem = otNewtype int4 unInt4 quotRem
+                             toInteger = toInteger . unInt4
+
+instance Integral Word1 where quotRem = otNewtype word1 unWord1 quotRem
+                              toInteger = toInteger . unWord1
+
+instance Integral Word2 where quotRem = otNewtype word2 unWord2 quotRem
+                              toInteger = toInteger . unWord2
+
+instance Integral Word3 where quotRem = otNewtype word3 unWord3 quotRem
+                              toInteger = toInteger . unWord3
+
+instance Integral Word4 where quotRem = otNewtype word4 unWord4 quotRem
+                              toInteger = toInteger . unWord4
+
+instance Integral Nat where quotRem = otNewtype Nat unNat quotRem
+                            toInteger = toInteger . unNat
+
+instance Integral Nat1 where quotRem = otNewtype nat1 unNat1 quotRem
+                             toInteger = toInteger . unNat1
+
+instance Integral Nat2 where quotRem = otNewtype nat2 unNat2 quotRem
+                             toInteger = toInteger . unNat2
+
+instance Integral Nat3 where quotRem = otNewtype nat3 unNat3 quotRem
+                             toInteger = toInteger . unNat3
+
+instance Integral Nat4 where quotRem = otNewtype nat4 unNat4 quotRem
+                             toInteger = toInteger . unNat4
+
+instance Integral Nat5 where quotRem = otNewtype nat5 unNat5 quotRem
+                             toInteger = toInteger . unNat5
+
+instance Integral Nat6 where quotRem = otNewtype nat6 unNat6 quotRem
+                             toInteger = toInteger . unNat6
+
+instance Integral Nat7 where quotRem = otNewtype nat7 unNat7 quotRem
+                             toInteger = toInteger . unNat7
+
+instance Bounded Int1 where maxBound = Int1 0; minBound = Int1 (-1)
+instance Bounded Int2 where maxBound = Int2 1; minBound = Int2 (-2)
+instance Bounded Int3 where maxBound = Int3 3; minBound = Int3 (-4)
+instance Bounded Int4 where maxBound = Int4 7; minBound = Int4 (-8)
+instance Bounded Word1 where maxBound = Word1 1; minBound = Word1 0
+instance Bounded Word2 where maxBound = Word2 3; minBound = Word2 0
+instance Bounded Word3 where maxBound = Word3 7; minBound = Word3 0
+instance Bounded Word4 where maxBound = Word4 15; minBound = Word4 0
+instance Bounded Nat1 where maxBound = Nat1 0; minBound = Nat1 0
+instance Bounded Nat2 where maxBound = Nat2 1; minBound = Nat2 0
+instance Bounded Nat3 where maxBound = Nat3 2; minBound = Nat3 0
+instance Bounded Nat4 where maxBound = Nat4 3; minBound = Nat4 0
+instance Bounded Nat5 where maxBound = Nat5 4; minBound = Nat5 0
+instance Bounded Nat6 where maxBound = Nat6 5; minBound = Nat6 0
+instance Bounded Nat7 where maxBound = Nat7 6; minBound = Nat7 0
+
+instance Enum Int1 where toEnum   = int1;   enumFrom     = boundedEnumFrom
+                         fromEnum = unInt1; enumFromThen = boundedEnumFromThen
+
+instance Enum Int2 where toEnum   = int2;   enumFrom     = boundedEnumFrom
+                         fromEnum = unInt2; enumFromThen = boundedEnumFromThen
+
+instance Enum Int3 where toEnum   = int3;   enumFrom     = boundedEnumFrom
+                         fromEnum = unInt3; enumFromThen = boundedEnumFromThen
+
+instance Enum Int4 where toEnum   = int4;   enumFrom     = boundedEnumFrom
+                         fromEnum = unInt4; enumFromThen = boundedEnumFromThen
+
+instance Enum Word1 where toEnum   = word1;   enumFrom     = boundedEnumFrom
+                          fromEnum = unWord1; enumFromThen = boundedEnumFromThen
+
+instance Enum Word2 where toEnum   = word2;   enumFrom     = boundedEnumFrom
+                          fromEnum = unWord2; enumFromThen = boundedEnumFromThen
+
+instance Enum Word3 where toEnum   = word3;   enumFrom     = boundedEnumFrom
+                          fromEnum = unWord3; enumFromThen = boundedEnumFromThen
+
+instance Enum Word4 where toEnum   = word4;   enumFrom     = boundedEnumFrom
+                          fromEnum = unWord4; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat where
+  toEnum   = Nat;    enumFrom     (Nat x)         = map Nat [x..]
+  fromEnum = unNat;  enumFromThen (Nat x) (Nat s) = map Nat [x,s..]
+
+instance Enum Nat1 where toEnum   = nat1;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat1; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat2 where toEnum   = nat2;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat2; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat3 where toEnum   = nat3;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat3; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat4 where toEnum   = nat4;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat4; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat5 where toEnum   = nat5;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat5; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat6 where toEnum   = nat6;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat6; enumFromThen = boundedEnumFromThen
+
+instance Enum Nat7 where toEnum   = nat7;   enumFrom     = boundedEnumFrom
+                         fromEnum = unNat7; enumFromThen = boundedEnumFromThen
+
+instance Listable Int1 where list = [0,minBound]
+instance Listable Int2 where list = listIntegral
+instance Listable Int3 where list = listIntegral
+instance Listable Int4 where list = listIntegral
+instance Listable Word1 where list = [0..]
+instance Listable Word2 where list = [0..]
+instance Listable Word3 where list = [0..]
+instance Listable Word4 where list = [0..]
+instance Listable Nat where list = [0..]
+instance Listable Nat1 where list = [0..]
+instance Listable Nat2 where list = [0..]
+instance Listable Nat3 where list = [0..]
+instance Listable Nat4 where list = [0..]
+instance Listable Nat5 where list = [0..]
+instance Listable Nat6 where list = [0..]
+instance Listable Nat7 where list = [0..]
+
+type UInt1 = Word1
+type UInt2 = Word2
+type UInt3 = Word3
+type UInt4 = Word4
diff --git a/tests/test-derive.hs b/tests/test-derive.hs
new file mode 100644
--- /dev/null
+++ b/tests/test-derive.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE TemplateHaskell #-}
+import Test.LeanCheck.Derive
+import Test.LeanCheck
+import System.Exit (exitFailure)
+import Data.List (elemIndices)
+import Test.LeanCheck.Utils.Operators
+
+data D0       = D0                    deriving Show
+data D1 a     = D1 a                  deriving Show
+data D2 a b   = D2 a b                deriving Show
+data D3 a b c = D3 a b c              deriving Show
+data C1 a     =           C11 a | C10 deriving Show
+data C2 a b   = C22 a b | C21 a | C20 deriving Show
+data I a b    = a :+ b                deriving Show
+
+deriveListable ''D0
+deriveListable ''D1
+deriveListable ''D2
+deriveListable ''D3
+deriveListable ''C1
+deriveListable ''C2
+deriveListable ''I
+
+-- Those should have no effect (instance already exists):
+{- uncommenting those should generate warnings
+deriveListable ''Bool
+deriveListable ''Maybe
+deriveListable ''Either
+-}
+
+main :: IO ()
+main =
+  case elemIndices False (tests 100) of
+    [] -> putStrLn "Tests passed!"
+    is -> do putStrLn ("Failed tests:" ++ show is)
+             exitFailure
+
+tests n =
+  [ True
+
+  , map unD0 list =| n |= list
+  , map unD1 list =| n |= (list :: [Int])
+  , map unD2 list =| n |= (list :: [(Int,Int)])
+  , map unD3 list =| n |= (list :: [(Int,Int,Int)])
+
+  , map unD1 list == (list :: [()])
+  , map unD2 list == (list :: [((),())])
+  , map unD3 list == (list :: [((),(),())])
+
+  , map unD1 list == (list :: [Bool])
+  , map unD2 list == (list :: [(Bool,Bool)])
+  , map unD3 list == (list :: [(Bool,Bool,Bool)])
+  ]
+  where
+  unD0 (D0)       = ()
+  unD1 (D1 x)     = (x)
+  unD2 (D2 x y)   = (x,y)
+  unD3 (D3 x y z) = (x,y,z)
diff --git a/tests/test-error.hs b/tests/test-error.hs
--- a/tests/test-error.hs
+++ b/tests/test-error.hs
@@ -1,8 +1,8 @@
 import System.Exit (exitFailure)
 import Data.List (elemIndices,sort)
 
-import Test.Check.Error
-import Test.Types (Nat)
+import Test.LeanCheck.Error
+import Test.LeanCheck.Utils.Types (Nat)
 import Data.List (sort)
 
 main :: IO ()
diff --git a/tests/test-most.hs b/tests/test-most.hs
deleted file mode 100644
--- a/tests/test-most.hs
+++ /dev/null
@@ -1,34 +0,0 @@
--- Simple file just to test if everything is imported fine
-import System.Exit (exitFailure)
-import Data.List (elemIndices)
-
-import Test.Most
-import Test.Check.Invariants (strictlyOrdered)
-
-main :: IO ()
-main =
-  case elemIndices False tests of
-    [] -> putStrLn "Tests passed!"
-    is -> do putStrLn ("Failed tests:" ++ show is)
-             exitFailure
-
-tests =
-  [ True
-
-  -- Test.Check
-  , holds 1 True
-
-  -- Test.Check.Utils
-  , checkCrescent 1
-
-  -- Test.Types
-  , [minBound..maxBound :: UInt1] == [0,1]
-
-  -- Test.Operators
-  , holds 1 $ (not . not) === id
-  ]
-
-checkCrescent :: Int -> Bool
-checkCrescent n = strictlyAscendingListsOf (tiers :: [[Nat]])
-          =| n |= (map . filter) strictlyOrdered (tiers :: [[[Nat]]])
-
diff --git a/tests/test-operators.hs b/tests/test-operators.hs
--- a/tests/test-operators.hs
+++ b/tests/test-operators.hs
@@ -1,8 +1,7 @@
 import System.Exit (exitFailure)
 import Data.List (elemIndices,sort)
-import Test.Check
-import Test.Operators
-import Test.TypeBinding
+import Test.LeanCheck
+import Test.LeanCheck.Utils
 
 
 main :: IO ()
diff --git a/tests/test-types.hs b/tests/test-types.hs
--- a/tests/test-types.hs
+++ b/tests/test-types.hs
@@ -1,7 +1,7 @@
 import System.Exit (exitFailure)
 import Data.List (elemIndices,delete)
-import Test.Types
-import Test.Check (list,fails)
+import Test.LeanCheck.Utils.Types
+import Test.LeanCheck (list,fails)
 
 main :: IO ()
 main =
diff --git a/tests/test-utils.hs b/tests/test-utils.hs
--- a/tests/test-utils.hs
+++ b/tests/test-utils.hs
@@ -1,11 +1,9 @@
 import System.Exit (exitFailure)
 import Data.List (elemIndices, sort, nub, delete)
 
-import Test.Check
-import Test.Check.Invariants
-import Test.Operators
-import Test.TypeBinding
-import Test.Types (Nat)
+import Test.LeanCheck
+import Test.LeanCheck.Invariants
+import Test.LeanCheck.Utils
 
 
 main :: IO ()
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -1,11 +1,9 @@
 import System.Exit (exitFailure)
 import Data.List (elemIndices)
 
-import Test.Check
-import Test.Check.Invariants
-import Test.Types (Nat)
-import Test.Operators
-import Test.TypeBinding
+import Test.LeanCheck
+import Test.LeanCheck.Invariants
+import Test.LeanCheck.Utils
 
 main :: IO ()
 main =