diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -1,6 +1,6 @@
 # Builds and tests this Haskell project on "GitHub Actions"
 #
-# 2021-2024  Rudy Matela
+# 2021-2025  Rudy Matela
 #
 # some docs: https://github.com/haskell-actions/setup
 #
diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,6 @@
 # gitignore for Conjure
 #
-# Part of Conjure, Copyright 2021-2024  Rudy Matela,
+# Part of Conjure, Copyright 2021-2025  Rudy Matela,
 # distribued under the 3-clause BSD license.
 
 # temporary files
@@ -50,6 +50,7 @@
 eg/bst
 eg/replicate
 eg/setelem
+eg/take-drop
 eg/sort
 eg/subset
 eg/spec
@@ -59,7 +60,6 @@
 bench/self
 bench/longshot
 bench/ill-hit
-bench/take-drop
 bench/p12
 bench/p30
 bench/candidates
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2021-2024, Rudy Matela
+Copyright (c) 2021-2025, Rudy Matela
 
 All rights reserved.
 
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -11,7 +11,7 @@
   -i $(shell find ~/.cabal -name leancheck.haddock | tail -1) \
   -i $(shell find ~/.cabal -name express.haddock   | tail -1) \
   -i $(shell find ~/.cabal -name speculate.haddock | tail -1) \
-  -i $(shell find /usr/share/doc/ghc/html/libraries -name template-haskell.haddock | tail -1) \
+  -i $(shell find /usr/share/doc/ghc*/html/libraries -name template-haskell.haddock | tail -1) \
   $(shell grep -q "Arch Linux" /etc/lsb-release && echo --optghc=-dynamic) \
   | grep -v "^Warning: Couldn't find .haddock for export [A-Z]$$"
 INSTALL_DEPS = leancheck express speculate template-haskell
@@ -38,6 +38,7 @@
   eg/pow \
   eg/replicate \
   eg/setelem \
+  eg/take-drop \
   eg/sort \
   eg/subset \
   eg/spec \
@@ -53,7 +54,6 @@
   bench/strategies \
   bench/self \
   bench/carry-on \
-  bench/take-drop \
   bench/p12 \
   bench/p30 \
   bench/gps \
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -49,86 +49,47 @@
 
 Then, declare a partial definition of a function to be synthesized.
 For example,
-here is a partial implementation of a function that squares a number:
+here is a partial implementation of a function that computes the factorial of a number:
 
-	square :: Int -> Int
-	square 0  =  0
-	square 1  =  1
-	square 2  =  4
+	factorial :: Int -> Int
+	factorial 1  =  1
+	factorial 2  =  2
+	factorial 3  =  6
+	factorial 4  =  24
 
 Next, declare a list of primitives that seem like interesting pieces
 in the final fully-defined implementation.
 For example,
 here is a list of primitives including
-addition, multiplication and their neutral elements:
+addition, multiplication, subtraction and their neutral elements:
 
 	primitives :: [Prim]
 	primitives  =  [ pr (0::Int)
 	               , pr (1::Int)
 	               , prim "+" ((+) :: Int -> Int -> Int)
 	               , prim "*" ((*) :: Int -> Int -> Int)
+	               , prim "-" ((-) :: Int -> Int -> Int)
 	               ]
 
 Finally, call the [`conjure`] function,
 passing the function name, the partial definition and the list of primitives:
 
-	> conjure "square" square primitives
-	square :: Int -> Int
-	-- testing 3 combinations of argument values
-	-- pruning with 14/25 rules
-	-- looking through 3 candidates of size 1
-	-- looking through 4 candidates of size 2
-	-- looking through 9 candidates of size 3
-	square x  =  x * x
-
-Conjure is able to synthesize the above implementation in less than a second.
-
-For more information, see the `eg/arith.hs` example and
-the Haddock documentation for the [`conjure`] and [`conjureWith`] functions.
-
-
-Synthesizing recursive functions
---------------------------------
-
-Conjure supports synthetization of recursive functions.
-
-Take for example the following partial implementation of a function
-that computes the factorial of a number:
-
 	factorial :: Int -> Int
-	factorial 1  =  1
-	factorial 2  =  2
-	factorial 3  =  6
-	factorial 4  =  24
-
-Here is a list of primitives:
-
-	primitives :: [Prim]
-	primitives  =  [ pr (0::Int)
-	               , pr (1::Int)
-	               , prim "+" ((+) :: Int -> Int -> Int)
-	               , prim "*" ((*) :: Int -> Int -> Int)
-	               , prim "-" ((-) :: Int -> Int -> Int)
-	               ]
-
-And here is what Conjure produces
-with the above partial definition and list of primitives:
-
-	> conjure "factorial" factorial primitives
-	factorial :: Int -> Int
 	-- testing 4 combinations of argument values
 	-- pruning with 27/65 rules
 	-- looking through 3 candidates of size 1
-	-- looking through 4 candidates of size 2
-	-- looking through 13 candidates of size 3
-	-- looking through 34 candidates of size 4
-	-- looking through 75 candidates of size 5
-	-- looking through 183 candidates of size 6
-	-- looking through 577 candidates of size 7
+	-- looking through 3 candidates of size 2
+	-- looking through 7 candidates of size 3
+	-- looking through 8 candidates of size 4
+	-- looking through 28 candidates of size 5
+	-- looking through 35 candidates of size 6
+	-- looking through 167 candidates of size 7
+	-- tested 95 candidates
 	factorial 0  =  1
 	factorial x  =  x * factorial (x - 1)
 
-The above synthetization takes less than a second.
+Conjure is able to synthesize the above implementation in less than a second
+in a regular laptop computer.
 
 It is also possible to generate a folding implementation
 like the following:
@@ -141,6 +102,47 @@
 the Haddock documentation for the [`conjure`] and [`conjureWith`] functions.
 
 
+Synthesizing functions over algebraic data types
+------------------------------------------------
+
+Conjure is not limited to integers,
+it works for functions over algebraic data types too.
+Consider the following partial definition of `take`:
+
+	take' :: Int -> [a] -> [a]
+	take' 0 [x]    =  []
+	take' 1 [x]    =  [x]
+	take' 0 [x,y]  =  []
+	take' 1 [x,y]  =  [x]
+	take' 2 [x,y]  =  [x,y]
+	take' 3 [x,y]  =  [x,y]
+
+Conjure is able to find an appropriate implementation
+given list constructors, zero, one and subtraction:
+
+	> conjure "take" (take' :: Int -> [A] -> [A])
+	>   [ pr (0 :: Int)
+	>   , pr (1 :: Int)
+	>   , pr ([] :: [A])
+	>   , prim ":" ((:) :: A -> [A] -> [A])
+	>   , prim "-" ((-) :: Int -> Int -> Int)
+	>   ]
+	take :: Int -> [A] -> [A]
+	-- testing 153 combinations of argument values
+	-- pruning with 4/7 rules
+	-- ...  ...  ...
+	-- looking through 58 candidates of size 9
+	-- tested 104 candidates
+	take 0 xs  =  []
+	take x []  =  []
+	take x (y:xs)  =  y:take (x - 1) xs
+
+The above example also takes less than a second to run in a modern laptop.
+The selection of functions in the list of primitives was minimized
+to what was absolutely needed here.
+With a larger collection as primitives YMMV.
+
+
 Synthesizing from specifications (for advanced users)
 -----------------------------------------------------
 
@@ -156,6 +158,9 @@
 Take for example a function `duplicates :: Eq a => [a] -> [a]`
 that should return the duplicate elements in a list without repetitions.
 
+We will first try to use a partial definition to arrive at an appropriate result.
+Then we'll see how to use [`conjureFromSpec`].
+
 Let's start with the primitives:
 
 	primitives :: [Prim]
@@ -368,7 +373,7 @@
 contains more than 60 examples of use.
 
 
-Conjure, Copyright 2021-2024  Rudy Matela,
+Conjure, Copyright 2021-2025  Rudy Matela,
 distribued under the 3-clause BSD license.
 
 
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,5 +1,5 @@
 -- Setup.hs for code-conjure / Conjure
--- Part of Conjure, Copyright 2021-2024  Rudy Matela,
+-- Part of Conjure, Copyright 2021-2025  Rudy Matela,
 -- distribued under the 3-clause BSD license.
 import Distribution.Simple
 main = defaultMain
diff --git a/TODO.md b/TODO.md
--- a/TODO.md
+++ b/TODO.md
@@ -3,8 +3,7 @@
 
 A non-exhaustive list of things TO DO for Conjure.
 
-* improve documentation of `conjureIsDeconstruction`.
-  Document behaviour outside of function, not inside of it.
+* consider the size of patterns to thin-out each size partition
 
 * consider non top-level cases
 
@@ -23,7 +22,9 @@
 and we would avoid some `prif` hacks
 needed to conjure some functions.
 
+The one downside is that this would take a few days of work to implement.
 
+
 This file is part of Conjure,
-(C) 2021-2024 Rudy Matela,
+(C) 2021-2025 Rudy Matela,
 Distribued under the 3-Clause BSD license.
diff --git a/bench/avgs.hs b/bench/avgs.hs
--- a/bench/avgs.hs
+++ b/bench/avgs.hs
@@ -1,6 +1,6 @@
 -- Computes averages of several benchmarks
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Data.List
 import Data.Function
diff --git a/bench/bench b/bench/bench
--- a/bench/bench
+++ b/bench/bench
@@ -2,7 +2,7 @@
 #
 # A more elaborate benchmark for p12 and p30
 #
-# Copyright (C) 2021-2024 Rudy Matela
+# Copyright (C) 2021-2025 Rudy Matela
 # Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 run1() {
diff --git a/bench/candidates.hs b/bench/candidates.hs
--- a/bench/candidates.hs
+++ b/bench/candidates.hs
@@ -1,6 +1,6 @@
 -- print candidates
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import Conjure.Engine
@@ -26,8 +26,8 @@
   csC  =  concat cssC
   css1  =  take m css1'
   cssC  =  take m cssC'
-  (css1', thy)  =  candidateDefns1 args nm f ps
-  (cssC', _)    =  candidateDefnsC args nm f ps
+  (css1', thy, _)  =  candidateDefns1 args nm f ps
+  (cssC', _, _)    =  candidateDefnsC args nm f ps
   nRules  =  length (rules thy)
   nREs  =  length (equations thy) + nRules
 
diff --git a/bench/candidates.txt b/bench/candidates.txt
--- a/bench/candidates.txt
+++ b/bench/candidates.txt
@@ -1,7 +1,7 @@
 Candidates for: foo :: Int -> Int
   pruning with 27/65 rules
   [3,0,8,0,30,0,177,0,1203] direct candidates, 0 duplicates
-  [3,3,9,10,32,39,185,233,1169] pattern candidates, 0 duplicates
+  [3,3,9,10,32,39,185,217,1169] pattern candidates, 0 duplicates
 
 rules:
 x - x == 0
diff --git a/bench/carry-on.hs b/bench/carry-on.hs
--- a/bench/carry-on.hs
+++ b/bench/carry-on.hs
@@ -1,6 +1,6 @@
 -- carryon.hs: conjuring implementations of a factorial function
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/bench/carry-on.txt b/bench/carry-on.txt
--- a/bench/carry-on.txt
+++ b/bench/carry-on.txt
@@ -12,36 +12,32 @@
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
--- looking through 203 candidates of size 8
--- tested 254 candidates
-factorial 1  =  1
-factorial x  =  x * factorial (x - 1)
-
+-- looking through 195 candidates of size 8
 -- looking through 1048 candidates of size 9
--- tested 547 candidates
+-- tested 539 candidates
 factorial 0  =  0
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- tested 555 candidates
+-- tested 547 candidates
 factorial 0  =  1
 factorial 1  =  1
 factorial x  =  x * factorial (x - 1)
 
--- looking through 1301 candidates of size 10
--- looking through 7201 candidates of size 11
--- tested 3216 candidates
+-- looking through 1256 candidates of size 10
+-- looking through 7198 candidates of size 11
+-- tested 3160 candidates
 factorial 0  =  1
 factorial x  =  x + x * (factorial (x - 1) - 1)
 
--- tested 3396 candidates
+-- tested 3340 candidates
 factorial 0  =  1
 factorial x  =  x - x * (1 - factorial (x - 1))
 
--- tested 3519 candidates
+-- tested 3463 candidates
 factorial 0  =  1
 factorial x  =  (0 - x) * (0 - factorial (x - 1))
 
--- tested 10004 candidates
+-- tested 9948 candidates
 cannot conjure
 
diff --git a/bench/erroneous.hs b/bench/erroneous.hs
--- a/bench/erroneous.hs
+++ b/bench/erroneous.hs
@@ -1,6 +1,6 @@
 -- Print erroneous candidates
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2024-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -40,7 +40,7 @@
   css            =  take n
                  .  discardT isRedundantByIntroduction -- additional pruning rule
                  $  css'
-  (css', thy)    =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
   nRules         =  length (rules thy)
   nREs           =  length (equations thy) + nRules
   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark
diff --git a/bench/gps.hs b/bench/gps.hs
--- a/bench/gps.hs
+++ b/bench/gps.hs
@@ -1,6 +1,6 @@
 -- gps.hs: General Program Synthesis Benchmark Suite
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE CPP #-}
 import Conjure
diff --git a/bench/gps.txt b/bench/gps.txt
--- a/bench/gps.txt
+++ b/bench/gps.txt
@@ -305,9 +305,9 @@
 -- looking through 28 candidates of size 5
 -- looking through 35 candidates of size 6
 -- looking through 167 candidates of size 7
--- looking through 203 candidates of size 8
+-- looking through 195 candidates of size 8
 -- looking through 1048 candidates of size 9
--- tested 466 candidates
+-- tested 458 candidates
 gps17 0  =  0
 gps17 x  =  gps17 (x - 1) + x * x
 
diff --git a/bench/gps2.hs b/bench/gps2.hs
--- a/bench/gps2.hs
+++ b/bench/gps2.hs
@@ -1,6 +1,6 @@
 -- gps2.hs: General Program Synthesis Benchmark Suite II
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE CPP, TemplateHaskell #-}
 #if __GLASGOW_HASKELL__ <= 710
diff --git a/bench/gps2.txt b/bench/gps2.txt
--- a/bench/gps2.txt
+++ b/bench/gps2.txt
@@ -320,13 +320,13 @@
 -- looking through 3 candidates of size 4
 -- looking through 11 candidates of size 5
 -- looking through 13 candidates of size 6
--- looking through 91 candidates of size 7
+-- looking through 85 candidates of size 7
 -- looking through 104 candidates of size 8
--- looking through 850 candidates of size 9
+-- looking through 811 candidates of size 9
 -- looking through 923 candidates of size 10
--- looking through 8902 candidates of size 11
+-- looking through 8602 candidates of size 11
 -- looking through 9662 candidates of size 12
--- tested 20562 candidates
+-- tested 20217 candidates
 cannot conjure
 
 gps22 :: Int -> [Char]
diff --git a/bench/longshot.hs b/bench/longshot.hs
--- a/bench/longshot.hs
+++ b/bench/longshot.hs
@@ -1,6 +1,6 @@
 -- longshot.hs: miscellaneous longshots
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/bench/lowtests.hs b/bench/lowtests.hs
--- a/bench/lowtests.hs
+++ b/bench/lowtests.hs
@@ -1,6 +1,6 @@
 -- lowtests.hs: conjuring with a low number of tests
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 --
 -- With a low number of tests Conjure may not be able to find the actual
diff --git a/bench/p12.hs b/bench/p12.hs
--- a/bench/p12.hs
+++ b/bench/p12.hs
@@ -1,6 +1,6 @@
 -- 12 background primitives
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import System.Environment
diff --git a/bench/p12.txt b/bench/p12.txt
--- a/bench/p12.txt
+++ b/bench/p12.txt
@@ -7,7 +7,7 @@
 -- looking through 6 candidates of size 3
 -- looking through 13 candidates of size 4
 -- looking through 40 candidates of size 5
--- looking through 138 candidates of size 6
+-- looking through 137 candidates of size 6
 -- tested 69 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (dec x)
diff --git a/bench/p30.hs b/bench/p30.hs
--- a/bench/p30.hs
+++ b/bench/p30.hs
@@ -1,6 +1,6 @@
 -- 30 background primitives, does Conjure scale?
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import System.Environment
diff --git a/bench/redundants.hs b/bench/redundants.hs
--- a/bench/redundants.hs
+++ b/bench/redundants.hs
@@ -1,6 +1,6 @@
 -- Print redundant candidates
 --
--- Copyright (C) 2023-2024 Rudy Matela
+-- Copyright (C) 2023-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -40,7 +40,7 @@
   css            =  take n
                  .  discardT isRedundantByIntroduction -- additional pruning rule
                  $  css'
-  (css', thy)    =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
   nRules         =  length (rules thy)
   nREs           =  length (equations thy) + nRules
   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark
diff --git a/bench/runtime/lapmatrud/bench/candidates.runtime b/bench/runtime/lapmatrud/bench/candidates.runtime
--- a/bench/runtime/lapmatrud/bench/candidates.runtime
+++ b/bench/runtime/lapmatrud/bench/candidates.runtime
@@ -1,1 +1,1 @@
-9.9
+9.5
diff --git a/bench/runtime/lapmatrud/bench/carry-on.runtime b/bench/runtime/lapmatrud/bench/carry-on.runtime
--- a/bench/runtime/lapmatrud/bench/carry-on.runtime
+++ b/bench/runtime/lapmatrud/bench/carry-on.runtime
@@ -1,1 +1,1 @@
-2.5
+1.8
diff --git a/bench/runtime/lapmatrud/bench/gps.runtime b/bench/runtime/lapmatrud/bench/gps.runtime
--- a/bench/runtime/lapmatrud/bench/gps.runtime
+++ b/bench/runtime/lapmatrud/bench/gps.runtime
@@ -1,1 +1,1 @@
-14.7
+13.7
diff --git a/bench/runtime/lapmatrud/bench/gps2.runtime b/bench/runtime/lapmatrud/bench/gps2.runtime
--- a/bench/runtime/lapmatrud/bench/gps2.runtime
+++ b/bench/runtime/lapmatrud/bench/gps2.runtime
@@ -1,1 +1,1 @@
-12.5
+11.6
diff --git a/bench/runtime/lapmatrud/bench/ill-hit.runtime b/bench/runtime/lapmatrud/bench/ill-hit.runtime
--- a/bench/runtime/lapmatrud/bench/ill-hit.runtime
+++ b/bench/runtime/lapmatrud/bench/ill-hit.runtime
@@ -1,1 +1,1 @@
-0.5
+0.4
diff --git a/bench/runtime/lapmatrud/bench/redundants.runtime b/bench/runtime/lapmatrud/bench/redundants.runtime
--- a/bench/runtime/lapmatrud/bench/redundants.runtime
+++ b/bench/runtime/lapmatrud/bench/redundants.runtime
@@ -1,1 +1,1 @@
-3.0
+2.8
diff --git a/bench/runtime/lapmatrud/bench/strategies.runtime b/bench/runtime/lapmatrud/bench/strategies.runtime
--- a/bench/runtime/lapmatrud/bench/strategies.runtime
+++ b/bench/runtime/lapmatrud/bench/strategies.runtime
@@ -1,1 +1,1 @@
-4.5
+4.4
diff --git a/bench/runtime/lapmatrud/bench/take-drop.runtime b/bench/runtime/lapmatrud/bench/take-drop.runtime
deleted file mode 100644
--- a/bench/runtime/lapmatrud/bench/take-drop.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-0.3
diff --git a/bench/runtime/lapmatrud/bench/terpret.runtime b/bench/runtime/lapmatrud/bench/terpret.runtime
--- a/bench/runtime/lapmatrud/bench/terpret.runtime
+++ b/bench/runtime/lapmatrud/bench/terpret.runtime
@@ -1,1 +1,1 @@
-8.5
+7.7
diff --git a/bench/runtime/lapmatrud/bench/unique.runtime b/bench/runtime/lapmatrud/bench/unique.runtime
--- a/bench/runtime/lapmatrud/bench/unique.runtime
+++ b/bench/runtime/lapmatrud/bench/unique.runtime
@@ -1,1 +1,1 @@
-2.3
+2.1
diff --git a/bench/runtime/lapmatrud/bench/weird.runtime b/bench/runtime/lapmatrud/bench/weird.runtime
--- a/bench/runtime/lapmatrud/bench/weird.runtime
+++ b/bench/runtime/lapmatrud/bench/weird.runtime
@@ -1,1 +1,1 @@
-2.8
+2.6
diff --git a/bench/runtime/lapmatrud/eg/bools.runtime b/bench/runtime/lapmatrud/eg/bools.runtime
--- a/bench/runtime/lapmatrud/eg/bools.runtime
+++ b/bench/runtime/lapmatrud/eg/bools.runtime
@@ -1,1 +1,1 @@
-1.8
+1.3
diff --git a/bench/runtime/lapmatrud/eg/bst.runtime b/bench/runtime/lapmatrud/eg/bst.runtime
--- a/bench/runtime/lapmatrud/eg/bst.runtime
+++ b/bench/runtime/lapmatrud/eg/bst.runtime
@@ -1,1 +1,1 @@
-7.5
+7.6
diff --git a/bench/runtime/lapmatrud/eg/dupos.runtime b/bench/runtime/lapmatrud/eg/dupos.runtime
--- a/bench/runtime/lapmatrud/eg/dupos.runtime
+++ b/bench/runtime/lapmatrud/eg/dupos.runtime
@@ -1,1 +1,1 @@
-3.5
+3.2
diff --git a/bench/runtime/lapmatrud/eg/factorial.runtime b/bench/runtime/lapmatrud/eg/factorial.runtime
--- a/bench/runtime/lapmatrud/eg/factorial.runtime
+++ b/bench/runtime/lapmatrud/eg/factorial.runtime
@@ -1,1 +1,1 @@
-1.4
+1.3
diff --git a/bench/runtime/lapmatrud/eg/fib01.runtime b/bench/runtime/lapmatrud/eg/fib01.runtime
--- a/bench/runtime/lapmatrud/eg/fib01.runtime
+++ b/bench/runtime/lapmatrud/eg/fib01.runtime
@@ -1,1 +1,1 @@
-1.5
+1.4
diff --git a/bench/runtime/lapmatrud/eg/fibonacci.runtime b/bench/runtime/lapmatrud/eg/fibonacci.runtime
--- a/bench/runtime/lapmatrud/eg/fibonacci.runtime
+++ b/bench/runtime/lapmatrud/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-3.5
+2.8
diff --git a/bench/runtime/lapmatrud/eg/higher.runtime b/bench/runtime/lapmatrud/eg/higher.runtime
--- a/bench/runtime/lapmatrud/eg/higher.runtime
+++ b/bench/runtime/lapmatrud/eg/higher.runtime
@@ -1,1 +1,1 @@
-0.7
+0.6
diff --git a/bench/runtime/lapmatrud/eg/ints.runtime b/bench/runtime/lapmatrud/eg/ints.runtime
--- a/bench/runtime/lapmatrud/eg/ints.runtime
+++ b/bench/runtime/lapmatrud/eg/ints.runtime
@@ -1,1 +1,1 @@
-0.6
+0.7
diff --git a/bench/runtime/lapmatrud/eg/list.runtime b/bench/runtime/lapmatrud/eg/list.runtime
--- a/bench/runtime/lapmatrud/eg/list.runtime
+++ b/bench/runtime/lapmatrud/eg/list.runtime
@@ -1,1 +1,1 @@
-1.1
+0.6
diff --git a/bench/runtime/lapmatrud/eg/pow.runtime b/bench/runtime/lapmatrud/eg/pow.runtime
--- a/bench/runtime/lapmatrud/eg/pow.runtime
+++ b/bench/runtime/lapmatrud/eg/pow.runtime
@@ -1,1 +1,1 @@
-4.2
+3.5
diff --git a/bench/runtime/lapmatrud/eg/replicate.runtime b/bench/runtime/lapmatrud/eg/replicate.runtime
--- a/bench/runtime/lapmatrud/eg/replicate.runtime
+++ b/bench/runtime/lapmatrud/eg/replicate.runtime
@@ -1,1 +1,1 @@
-0.3
+0.2
diff --git a/bench/runtime/lapmatrud/eg/setelem.runtime b/bench/runtime/lapmatrud/eg/setelem.runtime
--- a/bench/runtime/lapmatrud/eg/setelem.runtime
+++ b/bench/runtime/lapmatrud/eg/setelem.runtime
@@ -1,1 +1,1 @@
-1.2
+0.8
diff --git a/bench/runtime/lapmatrud/eg/sort.runtime b/bench/runtime/lapmatrud/eg/sort.runtime
--- a/bench/runtime/lapmatrud/eg/sort.runtime
+++ b/bench/runtime/lapmatrud/eg/sort.runtime
@@ -1,1 +1,1 @@
-1.3
+4.2
diff --git a/bench/runtime/lapmatrud/eg/take-drop.runtime b/bench/runtime/lapmatrud/eg/take-drop.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/lapmatrud/eg/take-drop.runtime
@@ -0,0 +1,1 @@
+0.3
diff --git a/bench/runtime/lapmatrud/eg/tapps.runtime b/bench/runtime/lapmatrud/eg/tapps.runtime
--- a/bench/runtime/lapmatrud/eg/tapps.runtime
+++ b/bench/runtime/lapmatrud/eg/tapps.runtime
@@ -1,1 +1,1 @@
-0.5
+0.4
diff --git a/bench/runtime/lapmatrud/eg/tree.runtime b/bench/runtime/lapmatrud/eg/tree.runtime
--- a/bench/runtime/lapmatrud/eg/tree.runtime
+++ b/bench/runtime/lapmatrud/eg/tree.runtime
@@ -1,1 +1,1 @@
-1.2
+1.4
diff --git a/bench/runtime/lapmatrud/versions b/bench/runtime/lapmatrud/versions
--- a/bench/runtime/lapmatrud/versions
+++ b/bench/runtime/lapmatrud/versions
@@ -1,4 +1,4 @@
-GHC 9.0.2
+GHC 9.2.8
 leancheck-1.0.2
-express-1.0.16
+express-1.0.18
 speculate-0.4.20
diff --git a/bench/runtime/zero/bench/candidates.runtime b/bench/runtime/zero/bench/candidates.runtime
--- a/bench/runtime/zero/bench/candidates.runtime
+++ b/bench/runtime/zero/bench/candidates.runtime
@@ -1,1 +1,1 @@
-19.5
+16.7
diff --git a/bench/runtime/zero/bench/carry-on.runtime b/bench/runtime/zero/bench/carry-on.runtime
--- a/bench/runtime/zero/bench/carry-on.runtime
+++ b/bench/runtime/zero/bench/carry-on.runtime
@@ -1,1 +1,1 @@
-4.5
+3.5
diff --git a/bench/runtime/zero/bench/erroneous.runtime b/bench/runtime/zero/bench/erroneous.runtime
--- a/bench/runtime/zero/bench/erroneous.runtime
+++ b/bench/runtime/zero/bench/erroneous.runtime
@@ -1,1 +1,1 @@
-5.0
+5.1
diff --git a/bench/runtime/zero/bench/gps.runtime b/bench/runtime/zero/bench/gps.runtime
--- a/bench/runtime/zero/bench/gps.runtime
+++ b/bench/runtime/zero/bench/gps.runtime
@@ -1,1 +1,1 @@
-29.6
+25.3
diff --git a/bench/runtime/zero/bench/gps2.runtime b/bench/runtime/zero/bench/gps2.runtime
--- a/bench/runtime/zero/bench/gps2.runtime
+++ b/bench/runtime/zero/bench/gps2.runtime
@@ -1,1 +1,1 @@
-22.6
+21.1
diff --git a/bench/runtime/zero/bench/ill-hit.runtime b/bench/runtime/zero/bench/ill-hit.runtime
--- a/bench/runtime/zero/bench/ill-hit.runtime
+++ b/bench/runtime/zero/bench/ill-hit.runtime
@@ -1,1 +1,1 @@
-0.9
+0.8
diff --git a/bench/runtime/zero/bench/p12.runtime b/bench/runtime/zero/bench/p12.runtime
--- a/bench/runtime/zero/bench/p12.runtime
+++ b/bench/runtime/zero/bench/p12.runtime
@@ -1,1 +1,1 @@
-3.1
+3.0
diff --git a/bench/runtime/zero/bench/redundants.runtime b/bench/runtime/zero/bench/redundants.runtime
--- a/bench/runtime/zero/bench/redundants.runtime
+++ b/bench/runtime/zero/bench/redundants.runtime
@@ -1,1 +1,1 @@
-6.1
+5.7
diff --git a/bench/runtime/zero/bench/take-drop.runtime b/bench/runtime/zero/bench/take-drop.runtime
deleted file mode 100644
--- a/bench/runtime/zero/bench/take-drop.runtime
+++ /dev/null
@@ -1,1 +0,0 @@
-0.6
diff --git a/bench/runtime/zero/bench/terpret.runtime b/bench/runtime/zero/bench/terpret.runtime
--- a/bench/runtime/zero/bench/terpret.runtime
+++ b/bench/runtime/zero/bench/terpret.runtime
@@ -1,1 +1,1 @@
-14.7
+14.1
diff --git a/bench/runtime/zero/bench/unique.runtime b/bench/runtime/zero/bench/unique.runtime
--- a/bench/runtime/zero/bench/unique.runtime
+++ b/bench/runtime/zero/bench/unique.runtime
@@ -1,1 +1,1 @@
-4.4
+4.3
diff --git a/bench/runtime/zero/bench/weird.runtime b/bench/runtime/zero/bench/weird.runtime
--- a/bench/runtime/zero/bench/weird.runtime
+++ b/bench/runtime/zero/bench/weird.runtime
@@ -1,1 +1,1 @@
-5.0
+4.9
diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime
--- a/bench/runtime/zero/eg/bools.runtime
+++ b/bench/runtime/zero/eg/bools.runtime
@@ -1,1 +1,1 @@
-3.3
+3.4
diff --git a/bench/runtime/zero/eg/bst.runtime b/bench/runtime/zero/eg/bst.runtime
--- a/bench/runtime/zero/eg/bst.runtime
+++ b/bench/runtime/zero/eg/bst.runtime
@@ -1,1 +1,1 @@
-14.5
+14.4
diff --git a/bench/runtime/zero/eg/dupos.runtime b/bench/runtime/zero/eg/dupos.runtime
--- a/bench/runtime/zero/eg/dupos.runtime
+++ b/bench/runtime/zero/eg/dupos.runtime
@@ -1,1 +1,1 @@
-6.9
+6.6
diff --git a/bench/runtime/zero/eg/factorial.runtime b/bench/runtime/zero/eg/factorial.runtime
--- a/bench/runtime/zero/eg/factorial.runtime
+++ b/bench/runtime/zero/eg/factorial.runtime
@@ -1,1 +1,1 @@
-2.5
+2.4
diff --git a/bench/runtime/zero/eg/fib01.runtime b/bench/runtime/zero/eg/fib01.runtime
--- a/bench/runtime/zero/eg/fib01.runtime
+++ b/bench/runtime/zero/eg/fib01.runtime
@@ -1,1 +1,1 @@
-2.7
+2.8
diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime
--- a/bench/runtime/zero/eg/fibonacci.runtime
+++ b/bench/runtime/zero/eg/fibonacci.runtime
@@ -1,1 +1,1 @@
-6.3
+5.4
diff --git a/bench/runtime/zero/eg/higher.runtime b/bench/runtime/zero/eg/higher.runtime
--- a/bench/runtime/zero/eg/higher.runtime
+++ b/bench/runtime/zero/eg/higher.runtime
@@ -1,1 +1,1 @@
-1.3
+1.2
diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime
--- a/bench/runtime/zero/eg/list.runtime
+++ b/bench/runtime/zero/eg/list.runtime
@@ -1,1 +1,1 @@
-2.1
+3.8
diff --git a/bench/runtime/zero/eg/maybe.runtime b/bench/runtime/zero/eg/maybe.runtime
--- a/bench/runtime/zero/eg/maybe.runtime
+++ b/bench/runtime/zero/eg/maybe.runtime
@@ -1,1 +1,1 @@
-0.5
+0.6
diff --git a/bench/runtime/zero/eg/oddeven.runtime b/bench/runtime/zero/eg/oddeven.runtime
--- a/bench/runtime/zero/eg/oddeven.runtime
+++ b/bench/runtime/zero/eg/oddeven.runtime
@@ -1,1 +1,1 @@
-2.9
+3.0
diff --git a/bench/runtime/zero/eg/pow.runtime b/bench/runtime/zero/eg/pow.runtime
--- a/bench/runtime/zero/eg/pow.runtime
+++ b/bench/runtime/zero/eg/pow.runtime
@@ -1,1 +1,1 @@
-8.8
+6.8
diff --git a/bench/runtime/zero/eg/replicate.runtime b/bench/runtime/zero/eg/replicate.runtime
--- a/bench/runtime/zero/eg/replicate.runtime
+++ b/bench/runtime/zero/eg/replicate.runtime
@@ -1,1 +1,1 @@
-0.7
+0.6
diff --git a/bench/runtime/zero/eg/sort.runtime b/bench/runtime/zero/eg/sort.runtime
--- a/bench/runtime/zero/eg/sort.runtime
+++ b/bench/runtime/zero/eg/sort.runtime
@@ -1,1 +1,1 @@
-2.4
+7.6
diff --git a/bench/runtime/zero/eg/take-drop.runtime b/bench/runtime/zero/eg/take-drop.runtime
new file mode 100644
--- /dev/null
+++ b/bench/runtime/zero/eg/take-drop.runtime
@@ -0,0 +1,1 @@
+0.6
diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime
--- a/bench/runtime/zero/eg/tree.runtime
+++ b/bench/runtime/zero/eg/tree.runtime
@@ -1,1 +1,1 @@
-2.3
+2.6
diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions
--- a/bench/runtime/zero/versions
+++ b/bench/runtime/zero/versions
@@ -1,4 +1,4 @@
-GHC 9.0.2
+GHC 9.2.8
 leancheck-1.0.2
-express-1.0.16
+express-1.0.18
 speculate-0.4.20
diff --git a/bench/self.hs b/bench/self.hs
--- a/bench/self.hs
+++ b/bench/self.hs
@@ -1,6 +1,6 @@
 -- self.hs: conjuring functions through themselves
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/bench/strategies.hs b/bench/strategies.hs
--- a/bench/strategies.hs
+++ b/bench/strategies.hs
@@ -1,6 +1,6 @@
 -- strategies.hs: conjuring factorial with different strategies
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/bench/strategies.txt b/bench/strategies.txt
--- a/bench/strategies.txt
+++ b/bench/strategies.txt
@@ -67,9 +67,9 @@
 -- looking through 12 candidates of size 3
 -- looking through 24 candidates of size 4
 -- looking through 37 candidates of size 5
--- looking through 72 candidates of size 6
+-- looking through 70 candidates of size 6
 -- looking through 196 candidates of size 7
--- tested 165 candidates
+-- tested 163 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -82,9 +82,9 @@
 -- looking through 12 candidates of size 3
 -- looking through 24 candidates of size 4
 -- looking through 47 candidates of size 5
--- looking through 82 candidates of size 6
+-- looking through 70 candidates of size 6
 -- looking through 342 candidates of size 7
--- tested 284 candidates
+-- tested 272 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -97,9 +97,9 @@
 -- looking through 21 candidates of size 3
 -- looking through 42 candidates of size 4
 -- looking through 302 candidates of size 5
--- looking through 602 candidates of size 6
+-- looking through 600 candidates of size 6
 -- looking through 6115 candidates of size 7
--- tested 1001 candidates
+-- tested 999 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
@@ -127,9 +127,9 @@
 -- looking through 21 candidates of size 3
 -- looking through 42 candidates of size 4
 -- looking through 330 candidates of size 5
--- looking through 630 candidates of size 6
+-- looking through 600 candidates of size 6
 -- looking through 7215 candidates of size 7
--- tested 1945 candidates
+-- tested 1915 candidates
 factorial 0  =  1
 factorial x  =  x * factorial (x - 1)
 
diff --git a/bench/take-drop.hs b/bench/take-drop.hs
deleted file mode 100644
--- a/bench/take-drop.hs
+++ /dev/null
@@ -1,49 +0,0 @@
--- based code sent by Colin Runciman
-import Conjure
-
-drop' :: Int -> [a] -> [a]
-drop' 0 []     =  []
-drop' 1 []     =  []
-drop' 0 [x,y]  =  [x,y]
-drop' 1 [x,y]  =  [y]
-drop' 2 [x,y]  =  []
-drop' 3 [x,y]  =  []
-drop' 0 [x,y,z]  =  [x,y,z]
-drop' 1 [x,y,z]  =  [y,z]
-drop' 2 [x,y,z]  =  [z]
-drop' 3 [x,y,z]  =  []
-
-take' :: Int -> [a] -> [a]
-take' 0 []     =  []
-take' 1 []     =  []
-take' 0 [x,y]  =  []
-take' 1 [x,y]  =  [x]
-take' 2 [x,y]  =  [x,y]
-take' 3 [x,y]  =  [x,y]
-
-main :: IO ()
-main = do
-  -- drop 0 []      =  []               -- 1
-  -- drop 0 (x:xs)  =  x : xs           -- 4
-  -- drop n []      =  []               -- 5
-  -- drop n (x:xs)  =  drop (x - 1) xs  -- 10
-  conjure "drop" (drop' :: Int -> [A] -> [A])
-    [ pr (0 :: Int)
-    , pr (1 :: Int)
-    , pr ([] :: [A])
-    , prim ":" ((:) :: A -> [A] -> [A])
-    , prim "-" ((-) :: Int -> Int -> Int)
-    ]
-
-  -- take 0 []  =  []                     -- 1
-  -- take 0 (x:xs)  =  []                 -- 2
-  -- take x []  =  []                     -- 3
-  -- take x (y:xs)  =  y:take (x - 1) xs  -- 10
-  conjureWithMaxSize 16 "take" (take' :: Int -> [A] -> [A])
-    [ pr (0 :: Int)
-    , pr (1 :: Int)
-    , pr ([] :: [A])
-    , prim "||" ((||) :: Bool -> Bool -> Bool)
-    , prim "-" ((-) :: Int -> Int -> Int)
-    , prim ":" ((:) :: A -> [A] -> [A])
-    ]
diff --git a/bench/take-drop.txt b/bench/take-drop.txt
deleted file mode 100644
--- a/bench/take-drop.txt
+++ /dev/null
@@ -1,32 +0,0 @@
-drop :: Int -> [A] -> [A]
--- testing 360 combinations of argument values
--- pruning with 4/7 rules
--- looking through 2 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 6 candidates of size 4
--- looking through 8 candidates of size 5
--- looking through 13 candidates of size 6
--- looking through 24 candidates of size 7
--- tested 39 candidates
-drop 0 xs  =  xs
-drop x []  =  []
-drop x (y:xs)  =  drop (x - 1) xs
-
-take :: Int -> [A] -> [A]
--- testing 143 combinations of argument values
--- pruning with 14/21 rules
--- looking through 2 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 6 candidates of size 4
--- looking through 8 candidates of size 5
--- looking through 13 candidates of size 6
--- looking through 24 candidates of size 7
--- looking through 31 candidates of size 8
--- looking through 59 candidates of size 9
--- tested 111 candidates
-take 0 xs  =  []
-take x []  =  []
-take x (y:xs)  =  y:take (x - 1) xs
-
diff --git a/bench/terpret.hs b/bench/terpret.hs
--- a/bench/terpret.hs
+++ b/bench/terpret.hs
@@ -1,6 +1,6 @@
 -- terpret.hs: Benchmark execution-model problems from TerpreT
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 --
 -- You can find the description of these exercises on:
diff --git a/bench/time b/bench/time
--- a/bench/time
+++ b/bench/time
@@ -2,7 +2,7 @@
 #
 # bench/time: runs a program, discards stdout and print name and runtime
 #
-# Copyright (C) 2021-2024 Rudy Matela
+# Copyright (C) 2021-2025 Rudy Matela
 # Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 printf "%-14s  " "$*"
diff --git a/bench/unique.hs b/bench/unique.hs
--- a/bench/unique.hs
+++ b/bench/unique.hs
@@ -1,6 +1,6 @@
 -- Print unique candidates
 --
--- Copyright (C) 2023-2024 Rudy Matela
+-- Copyright (C) 2023-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 --
 -- This can be used to track
@@ -46,7 +46,7 @@
   css            =  take n
                  $  discardT isRedundantByIntroduction -- additional pruning rule
                  $  css'
-  (css', thy)    =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
+  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates
   nRules         =  length (rules thy)
   nREs           =  length (equations thy) + nRules
   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark
diff --git a/bench/versions b/bench/versions
--- a/bench/versions
+++ b/bench/versions
@@ -2,7 +2,7 @@
 #
 # bench/versions: print versions of installed dependencies
 #
-# Copyright (C) 2021-2024  Rudy Matela
+# Copyright (C) 2021-2025  Rudy Matela
 # Distributed under the 3-Clause BSD licence (see the file LICENSE).
 get-ghc-v() {
     ghc --version | sed -e "s/.* version/GHC/"
diff --git a/bench/weird.hs b/bench/weird.hs
--- a/bench/weird.hs
+++ b/bench/weird.hs
@@ -1,10 +1,14 @@
 -- weird.hs: conjures some weird or unintuitive functions
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 --
 -- This file conjures some weird or unintuitive functions.
 -- It is here to make sure we do not overprune!
+--
+-- For simplicity,
+-- we do not use partial definitions here.
+-- We use fully defined functions to conjure themselves.
 import Conjure
 
 -- | xor for integers
@@ -20,6 +24,11 @@
   conjure "^^^" (^^^) primitives
   conjureWith args{usePatterns = False} "^^^" (^^^) primitives
 
+  -- This example is quite degenerate,
+  -- it takes a while to conjure even with just 2 primitives.
+  -- I am leaving it commented-out for now...
+  -- conjure "thirty" thirty [pr (0::Int), prim "+" ((+) :: Int -> Int -> Int)]
+
 primitives :: [Prim]
 primitives  =
   [ pr (0::Int)
@@ -31,3 +40,12 @@
   , prim "||" (||)
   , prif (undefined :: Int)
   ]
+
+-- | returns the sum when one of the arguments is 0
+--
+-- Naming: thirty/30, sum of __3__, when one is __0__
+thirty :: Int -> Int -> Int -> Int
+thirty 0 y z  =  y + z
+thirty x 0 z  =  x + z
+thirty x y 0  =  x + y
+thirty x y z  =  0
diff --git a/changelog.md b/changelog.md
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,21 @@
 ============================
 
 
+v0.6.0 (February 2025)
+----------------------
+
+* `Args` record: add `showCandidates`, `showTests` and `showDeconstructions`
+  to make it easier to see what Conjure is doing.
+* require `0` as a base case when recursing over `Num`s,
+  can be disabled by setting `requireZero=False` on `Args`.
+* `conjpure*`: return a record rather than a tuple.
+* improve main documentation and introductory examples in Haddock and README.
+* improve Haddock documentation a bit throughout
+  (`conjureIsDeconstruction`, `deriveConjurable`, etc).
+* slightly improve examples and benchmarks
+* (internal) improve debugging mechanisms of `Defn` evaluation functions.
+
+
 v0.5.16 (January 2025)
 ----------------------
 
diff --git a/code-conjure.cabal b/code-conjure.cabal
--- a/code-conjure.cabal
+++ b/code-conjure.cabal
@@ -1,9 +1,9 @@
 -- Cabal file for the Conjure program generation library.
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 name:                code-conjure
-version:             0.5.16
+version:             0.6.0
 synopsis:            synthesize Haskell functions out of partial definitions
 description:
   Conjure is a tool that synthesizes Haskell functions out of partial definitions.
@@ -52,7 +52,8 @@
                   , bench/time
                   , test/mk
                   , test/sdist
-tested-with: GHC==9.10
+tested-with: GHC==9.12
+           , GHC==9.10
            , GHC==9.8
            , GHC==9.6
            , GHC==9.4
@@ -67,7 +68,7 @@
 source-repository this
   type:            git
   location:        https://github.com/rudymatela/conjure
-  tag:             v0.5.16
+  tag:             v0.6.0
 
 library
   exposed-modules: Conjure
diff --git a/eg/arith.hs b/eg/arith.hs
--- a/eg/arith.hs
+++ b/eg/arith.hs
@@ -1,6 +1,6 @@
 -- arith.hs: conjuring simple non-recursive numeric functions
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/eg/bools.hs b/eg/bools.hs
--- a/eg/bools.hs
+++ b/eg/bools.hs
@@ -1,6 +1,6 @@
 -- bools.hs: simple recursive functions over boolean lists
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -30,29 +30,9 @@
   , prim "not" not
   , prim "||" (||)
   , prim "&&" (&&)
-  , prim "null" (null :: [Bool] -> Bool)
-  , prim "head" (head :: [Bool] -> Bool)
-  , prim "tail" (tail :: [Bool] -> [Bool])
   ]
 
 primitivesWithFold :: [Prim]
 primitivesWithFold  =
     prim "foldr" (foldr :: (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool)
   : primitives
-
--- target (for and):
-
--- and ps  =  if null ps then True else head ps && and (tail ps)
---            1  2    3       4         5    6  7  8    9    10 symbols
--- or
--- and ps  =  null ps || head ps && and (tail ps)
---            1    2  3  4    5  6  7    8    9 symbols
---
---
--- for or, we only reach the solution at size 11:
---
--- or' ps  =  not (null ps || not (head ps || or' (tail ps)))
---
--- unfortunately this is an ill-case,
--- I think there are smaller expressions that rewrite to the above bigger
--- expression so it is only found at the bigger size.
diff --git a/eg/bools.txt b/eg/bools.txt
--- a/eg/bools.txt
+++ b/eg/bools.txt
@@ -2,11 +2,11 @@
 -- testing 14 combinations of argument values
 -- pruning with 37/47 rules
 -- looking through 2 candidates of size 1
--- looking through 6 candidates of size 2
--- looking through 10 candidates of size 3
--- looking through 14 candidates of size 4
--- looking through 28 candidates of size 5
--- tested 38 candidates
+-- looking through 4 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 4 candidates of size 5
+-- tested 14 candidates
 and []  =  True
 and (p:ps)  =  p && and ps
 
@@ -14,31 +14,31 @@
 -- testing 14 combinations of argument values
 -- pruning with 37/47 rules
 -- looking through 2 candidates of size 1
--- looking through 6 candidates of size 2
--- looking through 10 candidates of size 3
--- looking through 14 candidates of size 4
--- looking through 28 candidates of size 5
--- tested 35 candidates
+-- looking through 4 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 4 candidates of size 5
+-- tested 11 candidates
 or []  =  False
 or (p:ps)  =  p || or ps
 
 and :: [Bool] -> Bool
 -- testing 14 combinations of argument values
--- pruning with 40/50 rules
+-- pruning with 39/49 rules
 -- looking through 2 candidates of size 1
--- looking through 6 candidates of size 2
--- looking through 10 candidates of size 3
--- looking through 16 candidates of size 4
--- tested 24 candidates
+-- looking through 4 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 4 candidates of size 4
+-- tested 12 candidates
 and ps  =  foldr (&&) True ps
 
 or :: [Bool] -> Bool
 -- testing 14 combinations of argument values
--- pruning with 40/50 rules
+-- pruning with 39/49 rules
 -- looking through 2 candidates of size 1
--- looking through 6 candidates of size 2
--- looking through 10 candidates of size 3
--- looking through 16 candidates of size 4
--- tested 23 candidates
+-- looking through 4 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 4 candidates of size 4
+-- tested 11 candidates
 or ps  =  foldr (||) False ps
 
diff --git a/eg/bst.hs b/eg/bst.hs
--- a/eg/bst.hs
+++ b/eg/bst.hs
@@ -1,6 +1,6 @@
 -- bst.hs: conjuring functions over binary search trees (BSTs)
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE CPP, TemplateHaskell #-}
 
diff --git a/eg/count.hs b/eg/count.hs
--- a/eg/count.hs
+++ b/eg/count.hs
@@ -39,13 +39,10 @@
     , prim "==" ((==) :: A -> A -> Bool)
     ]
 
-  conjureWithMaxSize 16 "count" count'
+  conjure "count" count'
     [ pr (0 :: Int)
     , pr (1 :: Int)
     , prim "+" ((+) :: Int -> Int -> Int)
-    , prim "head" (head :: [A] -> A)
-    , prim "tail" (tail :: [A] -> [A])
-    , prim "null" (null :: [A] -> Bool)
     , prim "==" ((==) :: A -> A -> Bool)
     , prif (undefined :: Int)
     ]
diff --git a/eg/count.txt b/eg/count.txt
--- a/eg/count.txt
+++ b/eg/count.txt
@@ -16,14 +16,14 @@
 -- looking through 2 candidates of size 2
 -- looking through 0 candidates of size 3
 -- looking through 0 candidates of size 4
--- looking through 2 candidates of size 5
--- looking through 10 candidates of size 6
--- looking through 20 candidates of size 7
--- looking through 54 candidates of size 8
--- looking through 130 candidates of size 9
--- looking through 298 candidates of size 10
--- looking through 629 candidates of size 11
--- tested 875 candidates
+-- looking through 0 candidates of size 5
+-- looking through 4 candidates of size 6
+-- looking through 4 candidates of size 7
+-- looking through 12 candidates of size 8
+-- looking through 20 candidates of size 9
+-- looking through 20 candidates of size 10
+-- looking through 52 candidates of size 11
+-- tested 79 candidates
 count x []  =  0
 count x (y:xs)  =  count x xs + (if x == y then 1 else 0)
 
diff --git a/eg/dupos.hs b/eg/dupos.hs
--- a/eg/dupos.hs
+++ b/eg/dupos.hs
@@ -1,6 +1,6 @@
 -- dupos.hs: duplicates and positions
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import Test.LeanCheck  -- needed for duplicatesSpec only
@@ -47,14 +47,6 @@
 
 main :: IO ()
 main = do
-  -- duplicates xs  =
-  --   if null xs                                                                   --  3
-  --   then []                                                                      --  4
-  --   else if head xs `elem` tail xs && not (head xs `elem` duplicates (tail xs))  -- 18
-  --        then head xs : duplicates (tail xs)                                     -- 24
-  --        else duplicates (tail xs)                                               -- 27
-  -- out of reach memory and performance wise
-  -- -- OR --
   -- duplicates []  =  []                                                  --  1
   -- duplicates (x:xs)  =  if x `elem` xs && not (x `elem` duplicates xs)  -- 11
   --                       then x : duplicates xs                          -- 15
diff --git a/eg/either.hs b/eg/either.hs
--- a/eg/either.hs
+++ b/eg/either.hs
@@ -1,6 +1,6 @@
 -- either.hs: conjuring functions over either values
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2024-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/eg/factorial.hs b/eg/factorial.hs
--- a/eg/factorial.hs
+++ b/eg/factorial.hs
@@ -1,6 +1,6 @@
 -- factorial.hs: conjuring a factorial function
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/eg/fib01.hs b/eg/fib01.hs
--- a/eg/fib01.hs
+++ b/eg/fib01.hs
@@ -1,4 +1,7 @@
 -- fib01.hs: conjuring an efficient fibonacci function
+--
+-- Copyright (C) 2021-2025 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
 fib01 :: Int -> Int -> Int -> Int
diff --git a/eg/fibonacci.hs b/eg/fibonacci.hs
--- a/eg/fibonacci.hs
+++ b/eg/fibonacci.hs
@@ -1,4 +1,7 @@
 -- fibonacci.hs: conjuring a fibonacci function
+--
+-- Copyright (C) 2021-2025 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
 fibonacci :: Int -> Int
diff --git a/eg/fibonacci.txt b/eg/fibonacci.txt
--- a/eg/fibonacci.txt
+++ b/eg/fibonacci.txt
@@ -8,12 +8,12 @@
 -- looking through 26 candidates of size 5
 -- looking through 27 candidates of size 6
 -- looking through 116 candidates of size 7
--- looking through 120 candidates of size 8
--- looking through 552 candidates of size 9
--- looking through 540 candidates of size 10
--- looking through 2663 candidates of size 11
--- looking through 2675 candidates of size 12
--- tested 4147 candidates
+-- looking through 102 candidates of size 8
+-- looking through 532 candidates of size 9
+-- looking through 474 candidates of size 10
+-- looking through 2571 candidates of size 11
+-- looking through 2287 candidates of size 12
+-- tested 3951 candidates
 fibonacci 0  =  1
 fibonacci 1  =  1
 fibonacci x  =  fibonacci (x - 1) + fibonacci (x - 2)
diff --git a/eg/gcd.hs b/eg/gcd.hs
--- a/eg/gcd.hs
+++ b/eg/gcd.hs
@@ -1,6 +1,6 @@
 -- gcd.hs: conjuring a GCD implementation
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -25,14 +25,3 @@
   -- desired function:
   -- gcd x 0  =  x
   -- gcd x y  =  gcd y (x `mod` y)
-
--- Degenerate case:
--- The number of candidates in this example is big,
--- if we set showTheory = True we can see why:
--- no properties are discovered.
---
--- Since
--- 0 `mod` 0 = undefined
--- Speculate has no way of discovering that
--- x `mod` x = 0
--- in all other cases.
diff --git a/eg/higher.hs b/eg/higher.hs
--- a/eg/higher.hs
+++ b/eg/higher.hs
@@ -1,6 +1,6 @@
 -- higher.hs: conjuring higher order functions
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2024-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/eg/id.hs b/eg/id.hs
--- a/eg/id.hs
+++ b/eg/id.hs
@@ -1,6 +1,6 @@
 -- id.hs: conjuring the identity and const functions
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2024-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/eg/ints.hs b/eg/ints.hs
--- a/eg/ints.hs
+++ b/eg/ints.hs
@@ -1,6 +1,6 @@
 -- ints.hs: conjuring functions over lists of ints
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -66,7 +66,3 @@
 primitivesWithFold  =
     prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)
   : primitives
-
--- sum xs      =  if null xs then 0 else head xs + sum (tail xs)
--- product xs  =  if null xs then 1 else head xs * product (tail xs)
---                1  2    3       4      5    6  7 8        9    10 symbols
diff --git a/eg/list.hs b/eg/list.hs
--- a/eg/list.hs
+++ b/eg/list.hs
@@ -1,6 +1,6 @@
 -- list.hs: conjuring functions over lists (of ints)
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -36,16 +36,6 @@
 [x,y] \/ [z,w]  =  [x,z,y,w]
 [x,y,z] \/ [w,v,u]  =  [x,w,y,v,z,u]
 
-merge' :: [Int] -> [Int] -> [Int]
-merge' [] []  =  []
-merge' xs []  =  xs
-merge' [] ys  =  ys
-merge' [x] [y] | x <= y     =  [x,y]
-               | otherwise  =  [y,x]
-merge' [0,1] [0,1]  =  [0,0,1,1]
-merge' [0,1] [2,3]  =  [0,1,2,3]
-merge' [0,2] [1,3]  =  [0,1,2,3]
-
 ordered' :: [Int] -> Bool
 ordered' []  =  True
 ordered' [x]  =  True
@@ -118,9 +108,5 @@
     , prim "tail" (tail :: [Int] -> [Int])
     ]
 
-  -- unreachable: needs about 26, but can only reach 16
-  conjureWithMaxSize 12 "merge" merge'
-    [ prim ":" ((:) :: Int -> [Int] -> [Int])
-    , prim "compare" (compare :: Int -> Int -> Ordering)
-    , primOrdCaseFor (undefined :: [Int])
-    ]
+  -- for elem, please see eg/setelem.hs
+  -- for take and drop, please see eg/take-drop.hs
diff --git a/eg/list.txt b/eg/list.txt
--- a/eg/list.txt
+++ b/eg/list.txt
@@ -111,21 +111,3 @@
 ordered []  =  True
 ordered (x:xs)  =  ordered xs && (null xs || x <= head xs)
 
-merge :: [Int] -> [Int] -> [Int]
--- testing 360 combinations of argument values
--- pruning with 1/2 rules
--- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 3 candidates of size 3
--- looking through 10 candidates of size 4
--- looking through 21 candidates of size 5
--- looking through 26 candidates of size 6
--- looking through 61 candidates of size 7
--- looking through 92 candidates of size 8
--- looking through 203 candidates of size 9
--- looking through 430 candidates of size 10
--- looking through 1086 candidates of size 11
--- looking through 2068 candidates of size 12
--- tested 4004 candidates
-cannot conjure
-
diff --git a/eg/maybe.hs b/eg/maybe.hs
--- a/eg/maybe.hs
+++ b/eg/maybe.hs
@@ -1,6 +1,6 @@
 -- maybe.hs: conjuring functions over maybe values
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
diff --git a/eg/oddeven.hs b/eg/oddeven.hs
--- a/eg/oddeven.hs
+++ b/eg/oddeven.hs
@@ -1,6 +1,6 @@
 -- oddeven.hs: conjuring even and odd from two sets of primitives
 --
--- Copyright (C) 2024 Rudy Matela
+-- Copyright (C) 2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import Prelude hiding (odd, even)
diff --git a/eg/pow.hs b/eg/pow.hs
--- a/eg/pow.hs
+++ b/eg/pow.hs
@@ -1,6 +1,6 @@
 -- pow.hs: conjuring exponentiation
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
@@ -22,9 +22,6 @@
     , prim "-" ((-) :: Int -> Int -> Int)
     ]
 
-  -- pow b e  =  if e == 0 then 1 else pow b (halve e) * pow b (halve e) * if odd e then b else 1
-  --             1  2  3 4      5      6   7  8     9 10 11 12  13   14 15 16 17  18    19     20
-  -- -- OR --
   -- pow b 0  =  1
   -- pow b e  =  pow b (halve e) * pow b (halve e) * if odd e then b else 1
   --             2   3  4     5  6 7   8  9    10 11 12 13 14     15     16
diff --git a/eg/pow.txt b/eg/pow.txt
--- a/eg/pow.txt
+++ b/eg/pow.txt
@@ -7,9 +7,9 @@
 -- looking through 159 candidates of size 4
 -- looking through 433 candidates of size 5
 -- looking through 1382 candidates of size 6
--- looking through 4136 candidates of size 7
+-- looking through 4118 candidates of size 7
 -- looking through 13292 candidates of size 8
--- tested 6383 candidates
+-- tested 6365 candidates
 pow x 0  =  1
 pow x y  =  x * pow x (y - 1)
 
@@ -21,7 +21,7 @@
 -- looking through 58 candidates of size 3
 -- looking through 174 candidates of size 4
 -- looking through 485 candidates of size 5
--- looking through 1387 candidates of size 6
--- tested 2126 candidates
+-- looking through 1369 candidates of size 6
+-- tested 2108 candidates
 cannot conjure
 
diff --git a/eg/replicate.hs b/eg/replicate.hs
--- a/eg/replicate.hs
+++ b/eg/replicate.hs
@@ -1,6 +1,6 @@
 -- replicate.hs: replicate and other functions
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import Data.List (transpose)
@@ -48,11 +48,8 @@
     ]
 
   -- alternative generation using recursion
-  conjureWith args{maxSize=13} "replicates" replicates'
+  conjure "replicates" replicates'
     [ pr ""
-    , prim "null" (null :: String -> Bool)
-    , prim "head" (head :: String -> Char)
-    , prim "tail" (tail :: String -> String)
     , prim ":" ((:) :: Char -> String -> String)
     , prim "++" ((++) :: String -> String -> String)
     , prim "replicate" (replicate :: Int -> Char -> String)
diff --git a/eg/replicate.txt b/eg/replicate.txt
--- a/eg/replicate.txt
+++ b/eg/replicate.txt
@@ -37,16 +37,16 @@
 
 replicates :: [Char] -> Int -> [Char]
 -- testing 360 combinations of argument values
--- pruning with 9/14 rules
+-- pruning with 4/4 rules
 -- looking through 2 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 7 candidates of size 3
--- looking through 22 candidates of size 4
--- looking through 59 candidates of size 5
--- looking through 152 candidates of size 6
--- looking through 442 candidates of size 7
--- looking through 1223 candidates of size 8
--- tested 736 candidates
+-- looking through 1 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 4 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 12 candidates of size 6
+-- looking through 1 candidates of size 7
+-- looking through 34 candidates of size 8
+-- tested 24 candidates
 replicates "" x  =  ""
 replicates (c:cs) x  =  replicate x c ++ replicates cs x
 
diff --git a/eg/setelem.hs b/eg/setelem.hs
--- a/eg/setelem.hs
+++ b/eg/setelem.hs
@@ -1,4 +1,7 @@
 -- setelem.hs: elem and set functions
+--
+-- Copyright (C) 2021-2025 Rudy Matela
+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 
 elem' :: Int -> [Int] -> Bool
@@ -14,9 +17,7 @@
 
 main :: IO ()
 main = do
-  -- elem x xs  =  not (null xs) && (elem x (tail xs) || x == head xs)
-  --               1    2    3    4  5    6   7   8   9  10 11 12  13
-  conjureWithMaxSize 13 "elem" (elem')
+  conjure "elem" (elem')
     [ pr ([] :: [Int])
     , pr True
     , pr False
@@ -24,15 +25,10 @@
     , prim "&&" (&&)
     , prim "not" not
     , prim ":" ((:) :: Int -> [Int] -> [Int])
-    , prim "head" (head :: [Int] -> Int)
-    , prim "tail" (tail :: [Int] -> [Int])
-    , prim "null" (null :: [Int] -> Bool)
     , prim "==" ((==) :: Int -> Int -> Bool)
     ]
 
-  -- set xs  =  null xs || set (tail xs) && not (elem (head xs) (tail xs))
-  --            1    2  3  4    5    6    7  8    9    10   11   12   13
-  conjureWithMaxSize 13 "set" (set')
+  conjure "set" (set')
     [ pr ([] :: [Int])
     , pr True
     , pr False
@@ -40,8 +36,5 @@
     , prim "||" (||)
     , prim "not" not
     , prim ":" ((:) :: Int -> [Int] -> [Int])
-    , prim "head" (head :: [Int] -> Int)
-    , prim "tail" (tail :: [Int] -> [Int])
-    , prim "null" (null :: [Int] -> Bool)
     , prim "elem" (elem :: Int -> [Int] -> Bool)
     ]
diff --git a/eg/setelem.txt b/eg/setelem.txt
--- a/eg/setelem.txt
+++ b/eg/setelem.txt
@@ -1,30 +1,30 @@
 elem :: Int -> [Int] -> Bool
 -- testing 360 combinations of argument values
--- pruning with 44/57 rules
+-- pruning with 40/53 rules
 -- looking through 2 candidates of size 1
--- looking through 3 candidates of size 2
--- looking through 5 candidates of size 3
--- looking through 16 candidates of size 4
--- looking through 38 candidates of size 5
--- looking through 67 candidates of size 6
--- looking through 134 candidates of size 7
--- looking through 345 candidates of size 8
--- tested 340 candidates
+-- looking through 2 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 6 candidates of size 5
+-- looking through 0 candidates of size 6
+-- looking through 0 candidates of size 7
+-- looking through 24 candidates of size 8
+-- tested 33 candidates
 elem x []  =  False
 elem x (y:xs)  =  elem x xs || x == y
 
 set :: [Int] -> Bool
 -- testing 360 combinations of argument values
--- pruning with 46/57 rules
+-- pruning with 41/52 rules
 -- looking through 2 candidates of size 1
--- looking through 2 candidates of size 2
--- looking through 4 candidates of size 3
--- looking through 10 candidates of size 4
--- looking through 20 candidates of size 5
--- looking through 41 candidates of size 6
--- looking through 100 candidates of size 7
--- looking through 234 candidates of size 8
--- tested 198 candidates
+-- looking through 1 candidates of size 2
+-- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 4
+-- looking through 1 candidates of size 5
+-- looking through 2 candidates of size 6
+-- looking through 4 candidates of size 7
+-- looking through 6 candidates of size 8
+-- tested 15 candidates
 set []  =  True
 set (x:xs)  =  set xs && not (elem x xs)
 
diff --git a/eg/sort.hs b/eg/sort.hs
--- a/eg/sort.hs
+++ b/eg/sort.hs
@@ -1,6 +1,6 @@
 -- sort.hs: conjuring a sort function
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 import Conjure
 import Data.List (insert, sort)
@@ -19,15 +19,28 @@
   | z <= x && x <= y  =  [z,x,y]
   | z <= y && y <= x  =  [z,y,x]
 
+insert' :: Int -> [Int] -> [Int]
+insert' 0 []  =  [0]
+insert' 0 [1,2]  =  [0,1,2]
+insert' 1 [0,2]  =  [0,1,2]
+insert' 2 [0,1]  =  [0,1,2]
+
+-- merge' :: [Int] -> [Int] -> [Int]
+-- merge' xs ys  =  sort (xs ++ ys)
+
 merge' :: [Int] -> [Int] -> [Int]
-merge' xs ys  =  sort (xs ++ ys)
+merge' [] []  =  []
+merge' xs []  =  xs
+merge' [] ys  =  ys
+merge' [x] [y] | x <= y     =  [x,y]
+               | otherwise  =  [y,x]
+merge' [0,1] [0,1]  =  [0,0,1,1]
+merge' [0,1] [2,3]  =  [0,1,2,3]
+merge' [0,2] [1,3]  =  [0,1,2,3]
 
 main :: IO ()
 main = do
   -- recursive insertion sort
-  -- sort xs  =  if null xs then [] else insert (head xs) (sort (tail xs))
-  --             1  2    3       4       5       6    7    8     9    10
-  -- -- OR --
   -- sort []  =  []
   -- sort (x:xs)  =  insert x (sort xs)
   conjure "sort" sort'
@@ -46,15 +59,14 @@
     , prim "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
     ]
 
-  -- qsort
-  -- qsort xs  =  if null xs                                 --  3
-  --              then []                                    --  4
-  --              else qsort (filter (< head xs) (tail xs))  -- 11
-  --                ++ (head xs:[])                          -- 16
-  --                ++ qsort (filter (>= head xs) (tail xs)) -- 24
-  -- not only this is out of reach performance wise,
-  -- but the needed recursive calls will not be enumerated
-  -- -- OR --
+  -- an insert function
+  conjureWithMaxSize 18 "insert" insert'
+    [ prim "[]" ([] :: [Int])
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "<=" ((<=) :: Int -> Int -> Bool)
+    , prif (undefined :: [Int])
+    ]
+
   -- qsort []  =  []                           -- 1
   -- qsort (x:xs)  =  qsort (filter (x >) xs)  -- 6
   --            ++ (x:qsort (filter (x <=) xs) -- 14
@@ -70,9 +82,20 @@
     , prim "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])
     ]
 
+  -- if we disable the descent requirement, we get the efficient qsort
+  -- though with a larger search space
+  conjureWith args{maxSize=14, requireDescent=False} "qsort" sort'
+    [ pr ([] :: [Int])
+    , prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])
+    , prim "<=" ((<=) :: Int -> Int -> Bool)
+    , prim ">"  ((>)  :: Int -> Int -> Bool)
+    , prim "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])
+    ]
+
   -- merge [] []  =  []
   -- merge (x:xs) (y:ys)  =  if x <= y then x:merge xs (y:ys) else y:merge (x:xs) ys
-  --                         2  3 4  5      678     9 10 11 12  13 14 15  16 17 18 19
+  --                         2  3 4  5      678     9 10 11 12  13 14 15 16 17 18 19
   -- OOM after size 17, out of reach performance wise
   -- update: cannot reach at size 19 on lapmatrud OOM
   conjureWith args{maxSize=12} "merge" merge'
@@ -80,4 +103,11 @@
     , prim ":" ((:) :: Int -> [Int] -> [Int])
     , prim "<=" ((<=) :: Int -> Int -> Bool)
     , prif (undefined :: [Int])
+    ]
+
+  -- unreachable: needs about 26, but can only reach 16
+  conjureWithMaxSize 12 "merge" merge'
+    [ prim ":" ((:) :: Int -> [Int] -> [Int])
+    , prim "compare" (compare :: Int -> Int -> Ordering)
+    , primOrdCaseFor (undefined :: [Int])
     ]
diff --git a/eg/sort.txt b/eg/sort.txt
--- a/eg/sort.txt
+++ b/eg/sort.txt
@@ -20,6 +20,32 @@
 -- tested 5 candidates
 sort xs  =  foldr insert [] xs
 
+insert :: Int -> [Int] -> [Int]
+-- testing 4 combinations of argument values
+-- pruning with 4/4 rules
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 2 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 2 candidates of size 5
+-- looking through 19 candidates of size 6
+-- looking through 6 candidates of size 7
+-- looking through 44 candidates of size 8
+-- looking through 62 candidates of size 9
+-- looking through 91 candidates of size 10
+-- looking through 334 candidates of size 11
+-- looking through 220 candidates of size 12
+-- looking through 1358 candidates of size 13
+-- looking through 1019 candidates of size 14
+-- looking through 4638 candidates of size 15
+-- looking through 6332 candidates of size 16
+-- looking through 14550 candidates of size 17
+-- tested 14943 candidates
+insert x []  =  [x]
+insert x (y:xs)  =  if x <= y
+                    then x:insert y xs
+                    else y:insert x xs
+
 qsort :: [Int] -> [Int]
 -- testing 360 combinations of argument values
 -- pruning with 8/8 rules
@@ -41,6 +67,27 @@
 qsort []  =  []
 qsort (x:xs)  =  filter (x >) (qsort xs) ++ (x:filter (x <=) (qsort xs))
 
+qsort :: [Int] -> [Int]
+-- testing 360 combinations of argument values
+-- pruning with 8/8 rules
+-- looking through 2 candidates of size 1
+-- looking through 1 candidates of size 2
+-- looking through 1 candidates of size 3
+-- looking through 3 candidates of size 4
+-- looking through 6 candidates of size 5
+-- looking through 9 candidates of size 6
+-- looking through 28 candidates of size 7
+-- looking through 51 candidates of size 8
+-- looking through 128 candidates of size 9
+-- looking through 303 candidates of size 10
+-- looking through 648 candidates of size 11
+-- looking through 1621 candidates of size 12
+-- looking through 3592 candidates of size 13
+-- looking through 8475 candidates of size 14
+-- tested 7794 candidates
+qsort []  =  []
+qsort (x:xs)  =  qsort (filter (x >) xs) ++ (x:qsort (filter (x <=) xs))
+
 merge :: [Int] -> [Int] -> [Int]
 -- testing 360 combinations of argument values
 -- pruning with 4/4 rules
@@ -57,5 +104,23 @@
 -- looking through 2972 candidates of size 11
 -- looking through 11011 candidates of size 12
 -- tested 17710 candidates
+cannot conjure
+
+merge :: [Int] -> [Int] -> [Int]
+-- testing 360 combinations of argument values
+-- pruning with 1/2 rules
+-- looking through 2 candidates of size 1
+-- looking through 2 candidates of size 2
+-- looking through 3 candidates of size 3
+-- looking through 10 candidates of size 4
+-- looking through 21 candidates of size 5
+-- looking through 26 candidates of size 6
+-- looking through 61 candidates of size 7
+-- looking through 92 candidates of size 8
+-- looking through 203 candidates of size 9
+-- looking through 430 candidates of size 10
+-- looking through 1086 candidates of size 11
+-- looking through 2068 candidates of size 12
+-- tested 4004 candidates
 cannot conjure
 
diff --git a/eg/spec.hs b/eg/spec.hs
--- a/eg/spec.hs
+++ b/eg/spec.hs
@@ -32,9 +32,6 @@
              && sum [1,2]   == 3
              && sum [3,4,5] == 12
 
--- hoping for something like
--- sum xs  =  if null xs then 0 else head xs + sum (tail xs)
-
 sumPrimitives :: [Prim]
 sumPrimitives  =
   [ prim "null" (null :: [Int] -> Bool)
@@ -49,9 +46,6 @@
 appSpec (++)  =  []      ++ [0,1]   == [0,1]
               && [2,3]   ++ []      == [2,3]
               && [4,5,6] ++ [7,8,9] == [4,5,6,7,8,9]
-
--- hoping for something like
--- app xs ys = if null xs then ys else head xs : app (tail xs) ys
 
 appPrimitives :: [Prim]
 appPrimitives =
diff --git a/eg/subset.hs b/eg/subset.hs
--- a/eg/subset.hs
+++ b/eg/subset.hs
@@ -1,6 +1,6 @@
 -- subset.hs: conjuring the subset function
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE CPP #-}
 import Conjure
@@ -41,9 +41,6 @@
 
 main :: IO ()
 main = do
-  -- subset xs ys  =  null xs || elem (head xs) ys && subset (tail xs) ys
-  --                  1    2  3  4     5    6   7  8  9       10   11  12
-  -- -- OR --
   -- subset [] ys  =  True
   -- subset (x:xs) ys  =  elem x ys && subset xs ys
   conjure "subset" (subset')
diff --git a/eg/take-drop.hs b/eg/take-drop.hs
new file mode 100644
--- /dev/null
+++ b/eg/take-drop.hs
@@ -0,0 +1,46 @@
+-- based code sent by Colin Runciman
+import Conjure
+
+drop' :: Int -> [a] -> [a]
+drop' 0 []     =  []
+drop' 1 []     =  []
+drop' 0 [x,y]  =  [x,y]
+drop' 1 [x,y]  =  [y]
+drop' 2 [x,y]  =  []
+drop' 3 [x,y]  =  []
+drop' 0 [x,y,z]  =  [x,y,z]
+drop' 1 [x,y,z]  =  [y,z]
+drop' 2 [x,y,z]  =  [z]
+drop' 3 [x,y,z]  =  []
+
+take' :: Int -> [a] -> [a]
+take' 0 [x]    =  []
+take' 1 [x]    =  [x]
+take' 0 [x,y]  =  []
+take' 1 [x,y]  =  [x]
+take' 2 [x,y]  =  [x,y]
+take' 3 [x,y]  =  [x,y]
+
+main :: IO ()
+main = do
+  -- drop 0 xs  =  xs                   -- 1
+  -- drop x []  =  []                   -- 2
+  -- drop x (y:xs)  =  drop (x - 1) xs  -- 7
+  conjure "drop" (drop' :: Int -> [A] -> [A])
+    [ pr (0 :: Int)
+    , pr (1 :: Int)
+    , pr ([] :: [A])
+    , prim ":" ((:) :: A -> [A] -> [A])
+    , prim "-" ((-) :: Int -> Int -> Int)
+    ]
+
+  -- take 0 xs  =  []                     -- 1
+  -- take x []  =  []                     -- 2
+  -- take x (y:xs)  =  y:take (x - 1) xs  -- 9
+  conjure "take" (take' :: Int -> [A] -> [A])
+    [ pr (0 :: Int)
+    , pr (1 :: Int)
+    , pr ([] :: [A])
+    , prim "-" ((-) :: Int -> Int -> Int)
+    , prim ":" ((:) :: A -> [A] -> [A])
+    ]
diff --git a/eg/take-drop.txt b/eg/take-drop.txt
new file mode 100644
--- /dev/null
+++ b/eg/take-drop.txt
@@ -0,0 +1,32 @@
+drop :: Int -> [A] -> [A]
+-- testing 360 combinations of argument values
+-- pruning with 4/7 rules
+-- looking through 2 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 8 candidates of size 5
+-- looking through 13 candidates of size 6
+-- looking through 22 candidates of size 7
+-- tested 39 candidates
+drop 0 xs  =  xs
+drop x []  =  []
+drop x (y:xs)  =  drop (x - 1) xs
+
+take :: Int -> [A] -> [A]
+-- testing 153 combinations of argument values
+-- pruning with 4/7 rules
+-- looking through 2 candidates of size 1
+-- looking through 3 candidates of size 2
+-- looking through 4 candidates of size 3
+-- looking through 6 candidates of size 4
+-- looking through 8 candidates of size 5
+-- looking through 13 candidates of size 6
+-- looking through 22 candidates of size 7
+-- looking through 26 candidates of size 8
+-- looking through 58 candidates of size 9
+-- tested 104 candidates
+take 0 xs  =  []
+take x []  =  []
+take x (y:xs)  =  y:take (x - 1) xs
+
diff --git a/eg/tapps.hs b/eg/tapps.hs
--- a/eg/tapps.hs
+++ b/eg/tapps.hs
@@ -1,6 +1,6 @@
 -- tapps.hs: conjure with (portable) type applications
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE CPP #-}
 #if __GLASGOW_HASKELL__ < 800
diff --git a/eg/tree.hs b/eg/tree.hs
--- a/eg/tree.hs
+++ b/eg/tree.hs
@@ -1,6 +1,6 @@
 -- tree.hs: conjuring functions over trees
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE CPP, TemplateHaskell #-}
 
@@ -127,7 +127,7 @@
     , prim "==" ((==) :: Int -> Int -> Bool)
     ]
 
-  -- unreachable: needs size 22 but OOMs at 18
+  -- unreachable: needs size 22 but OOMs at 19/20 (v0.5.16)
   conjureWithMaxSize 12 "ordered" ordered
     [ pr True
     , pr False
@@ -136,6 +136,7 @@
     , prim "<" ((<) :: Int -> Int -> Bool)
     , prim "rightmost" rightmost
     , prim "leftmost" leftmost
+    , prim "nil" nil
     ]
 
   conjure "ordered" ordered
diff --git a/eg/tree.txt b/eg/tree.txt
--- a/eg/tree.txt
+++ b/eg/tree.txt
@@ -83,18 +83,18 @@
 -- testing 360 combinations of argument values
 -- pruning with 29/39 rules
 -- looking through 2 candidates of size 1
--- looking through 1 candidates of size 2
--- looking through 0 candidates of size 3
+-- looking through 2 candidates of size 2
+-- looking through 2 candidates of size 3
 -- looking through 0 candidates of size 4
 -- looking through 10 candidates of size 5
--- looking through 20 candidates of size 6
+-- looking through 30 candidates of size 6
 -- looking through 0 candidates of size 7
--- looking through 32 candidates of size 8
--- looking through 80 candidates of size 9
+-- looking through 68 candidates of size 8
+-- looking through 216 candidates of size 9
 -- looking through 56 candidates of size 10
--- looking through 386 candidates of size 11
--- looking through 596 candidates of size 12
--- tested 1183 candidates
+-- looking through 802 candidates of size 11
+-- looking through 2077 candidates of size 12
+-- tested 3265 candidates
 cannot conjure
 
 ordered :: Tree -> Bool
diff --git a/mk/depend.mk b/mk/depend.mk
--- a/mk/depend.mk
+++ b/mk/depend.mk
@@ -224,23 +224,6 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   bench/strategies.hs
-bench/take-drop: \
-  bench/take-drop.hs \
-  mk/toplibs
-bench/take-drop.o: \
-  src/Conjure/Utils.hs \
-  src/Conjure/Red.hs \
-  src/Conjure/Reason.hs \
-  src/Conjure/Prim.hs \
-  src/Conjure.hs \
-  src/Conjure/Expr.hs \
-  src/Conjure/Engine.hs \
-  src/Conjure/Defn/Test.hs \
-  src/Conjure/Defn/Redundancy.hs \
-  src/Conjure/Defn.hs \
-  src/Conjure/Conjurable.hs \
-  src/Conjure/Conjurable/Derive.hs \
-  bench/take-drop.hs
 bench/terpret: \
   bench/terpret.hs \
   mk/toplibs
@@ -343,6 +326,40 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   eg/bst.hs
+eg/colin/IntFuns: \
+  eg/colin/IntFuns.hs \
+  mk/toplibs
+eg/colin/IntFuns.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Red.hs \
+  src/Conjure/Reason.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn/Test.hs \
+  src/Conjure/Defn/Redundancy.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  eg/colin/IntFuns.hs
+eg/colin/ListFuns: \
+  eg/colin/ListFuns.hs \
+  mk/toplibs
+eg/colin/ListFuns.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Red.hs \
+  src/Conjure/Reason.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn/Test.hs \
+  src/Conjure/Defn/Redundancy.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  eg/colin/ListFuns.hs
 eg/count: \
   eg/count.hs \
   mk/toplibs
@@ -666,6 +683,23 @@
   src/Conjure/Conjurable.hs \
   src/Conjure/Conjurable/Derive.hs \
   eg/subset.hs
+eg/take-drop: \
+  eg/take-drop.hs \
+  mk/toplibs
+eg/take-drop.o: \
+  src/Conjure/Utils.hs \
+  src/Conjure/Red.hs \
+  src/Conjure/Reason.hs \
+  src/Conjure/Prim.hs \
+  src/Conjure.hs \
+  src/Conjure/Expr.hs \
+  src/Conjure/Engine.hs \
+  src/Conjure/Defn/Test.hs \
+  src/Conjure/Defn/Redundancy.hs \
+  src/Conjure/Defn.hs \
+  src/Conjure/Conjurable.hs \
+  src/Conjure/Conjurable/Derive.hs \
+  eg/take-drop.hs
 eg/tapps: \
   eg/tapps.hs \
   mk/toplibs
diff --git a/proto/u-conjure.hs b/proto/u-conjure.hs
--- a/proto/u-conjure.hs
+++ b/proto/u-conjure.hs
@@ -4,7 +4,7 @@
 -- out of partially implemented functions.
 --
 --
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 --
 --
diff --git a/src/Conjure.hs b/src/Conjure.hs
--- a/src/Conjure.hs
+++ b/src/Conjure.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -8,16 +8,12 @@
 -- from tests or partial definitions.
 -- (a.k.a.: functional inductive programming)
 --
--- This is currently an experimental tool in its early stages,
--- don't expect much from its current version.
--- It is just a piece of curiosity in its current state.
---
 -- Step 1: declare your partial function
 --
--- > square :: Int -> Int
--- > square 0  =  0
--- > square 1  =  1
--- > square 2  =  4
+-- > factorial :: Int -> Int
+-- > factorial 2  =  2
+-- > factorial 3  =  6
+-- > factorial 4  =  24
 --
 -- Step 2: declare a list with the potential building blocks:
 --
@@ -27,18 +23,71 @@
 -- >   , pr (1::Int)
 -- >   , prim "+" ((+) :: Int -> Int -> Int)
 -- >   , prim "*" ((*) :: Int -> Int -> Int)
+-- >   , prim "-" ((-) :: Int -> Int -> Int)
 -- >   ]
 --
--- Step 3: call conjure and see your generated function:
+-- Step 3: call 'conjure' and see your generated function:
 --
--- > > conjure "square" square primitives
--- > square :: Int -> Int
+-- > > conjure "factorial" factorial primitives
+-- > factorial :: Int -> Int
 -- > -- testing 3 combinations of argument values
--- > -- pruning with 14/25 rules
+-- > -- pruning with 27/65 rules
 -- > -- looking through 3 candidates of size 1
--- > -- looking through 4 candidates of size 2
+-- > -- looking through 3 candidates of size 2
 -- > -- looking through 9 candidates of size 3
--- > square x  =  x * x
+-- > -- looking through 10 candidates of size 4
+-- > -- looking through 32 candidates of size 5
+-- > -- looking through 39 candidates of size 6
+-- > -- looking through 185 candidates of size 7
+-- > -- tested 107 candidates
+-- > factorial 0  =  1
+-- > factorial x  =  x * factorial (x - 1)
+--
+-- The above example takes less than a second to run in a modern laptop.
+--
+-- Factorial is discovered from scratch through a search.
+-- We prune the search space using properties discovered
+-- from the results of testing.
+--
+-- Conjure is not limited to integers,
+-- it works for functions over algebraic data types too.
+-- See:
+--
+-- > take' :: Int -> [a] -> [a]
+-- > take' 0 [x]    =  []
+-- > take' 1 [x]    =  [x]
+-- > take' 0 [x,y]  =  []
+-- > take' 1 [x,y]  =  [x]
+-- > take' 2 [x,y]  =  [x,y]
+-- > take' 3 [x,y]  =  [x,y]
+--
+-- > > conjure "take" (take' :: Int -> [A] -> [A])
+-- > >   [ pr (0 :: Int)
+-- > >   , pr (1 :: Int)
+-- > >   , pr ([] :: [A])
+-- > >   , prim ":" ((:) :: A -> [A] -> [A])
+-- > >   , prim "-" ((-) :: Int -> Int -> Int)
+-- > >   ]
+-- > take :: Int -> [A] -> [A]
+-- > -- testing 153 combinations of argument values
+-- > -- pruning with 4/7 rules
+-- > -- ...  ...  ...
+-- > -- looking through 58 candidates of size 9
+-- > -- tested 104 candidates
+-- > take 0 xs  =  []
+-- > take x []  =  []
+-- > take x (y:xs)  =  y:take (x - 1) xs
+--
+-- The above example also takes less than a second to run in a modern laptop.
+-- The selection of functions in the list of primitives was minimized
+-- to what was absolutely needed here.
+-- With a larger collection as primitives YMMV.
+--
+-- Conjure works for user-defined algebraic data types too,
+-- given that they are made instances of the 'Conjurable' typeclass.
+-- For types without data invariants,
+-- it should be enough to call 'deriveConjurable'
+-- to create an instance using TH.
 {-# LANGUAGE CPP #-}
 module Conjure
   (
@@ -55,9 +104,6 @@
   , conjureWith
   , Args(..)
   , args
-  , Expr
-  , val
-  , value
 
 -- * Conjuring from a specification
   , conjureFromSpec
@@ -65,6 +111,9 @@
 
 -- * When using custom types
   , Conjurable (conjureExpress, conjureEquality, conjureTiers, conjureCases, conjureSubTypes, conjureSize)
+  , Expr
+  , val
+  , value
   , reifyExpress
   , reifyEquality
   , reifyTiers
@@ -76,6 +125,7 @@
   , deriveConjurableCascading
 
 -- * Pure interfaces
+  , Results (..)
   , conjpure
   , conjpureWith
 
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
--- a/src/Conjure/Conjurable.hs
+++ b/src/Conjure/Conjurable.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Conjurable
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -110,6 +110,9 @@
 -- The @Proxy@ type was avoided for backwards compatibility.
 --
 -- Please see the source code of "Conjure.Conjurable" for more examples.
+--
+-- 'Conjurable' instances can be derived automatically using
+-- 'Conjure.deriveConjurable'.
 --
 -- (cf. 'reifyTiers', 'reifyEquality', 'conjureType')
 class (Typeable a, Name a) => Conjurable a where
diff --git a/src/Conjure/Conjurable/Derive.hs b/src/Conjure/Conjurable/Derive.hs
--- a/src/Conjure/Conjurable/Derive.hs
+++ b/src/Conjure/Conjurable/Derive.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE TemplateHaskell, CPP #-}
 -- |
 -- Module      : Conjure.Conjurable.Derive
--- Copyright   : (c) 2019-2024 Rudy Matela
+-- Copyright   : (c) 2019-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -27,21 +27,12 @@
 --
 -- This function needs the @TemplateHaskell@ extension.
 --
--- If '-:', '->:', '->>:', '->>>:', ... are not in scope,
--- this will derive them as well.
---
--- For now,
--- this function only derives
--- 'conjureEquality',
--- 'conjureTiers' and
--- 'conjureExpress'
--- and does not derive
--- 'conjureSubTypes',
--- 'conjureArgumentCases' and
--- 'conjureSize'.
--- These will be added in future versions.
--- If you plan to use features that depend on these functionalities,
--- please define your instances manually.
+-- If the "Data.Express"' type binding operators
+-- ('Data.Express.-:',
+--  'Data.Express.->:' or
+--  'Data.Express.->>:')
+-- are not in scope,
+-- this derives them as well.
 deriveConjurable :: Name -> DecsQ
 deriveConjurable  =  deriveWhenNeededOrWarn ''Conjurable reallyDerive
   where
@@ -49,19 +40,6 @@
 
 -- | Same as 'deriveConjurable' but does not warn when instance already exists
 --   ('deriveConjurable' is preferable).
---
--- For now,
--- this function only derives
--- 'conjureEquality',
--- 'conjureTiers' and
--- 'conjureExpress'
--- and does not derive
--- 'conjureSubTypes',
--- 'conjureArgumentCases' and
--- 'conjureSize'.
--- These will be added in future versions.
--- If you plan to use features that depend on these functionalities,
--- please define your instances manually.
 deriveConjurableIfNeeded :: Name -> DecsQ
 deriveConjurableIfNeeded  =  deriveWhenNeeded ''Conjurable reallyDerive
   where
@@ -69,19 +47,6 @@
 
 -- | Derives a 'Conjurable' instance for a given type 'Name'
 --   cascading derivation of type arguments as well.
---
--- For now,
--- this function only derives
--- 'conjureEquality',
--- 'conjureTiers' and
--- 'conjureExpress'
--- and does not derive
--- 'conjureSubTypes',
--- 'conjureArgumentCases' and
--- 'conjureSize'.
--- These will be added in future versions.
--- If you plan to use features that depend on these functionalities,
--- please define your instances manually.
 deriveConjurableCascading :: Name -> DecsQ
 deriveConjurableCascading  =  deriveWhenNeeded ''Conjurable reallyDerive
   where
diff --git a/src/Conjure/Defn.hs b/src/Conjure/Defn.hs
--- a/src/Conjure/Defn.hs
+++ b/src/Conjure/Defn.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Defn
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -136,8 +136,8 @@
 
   -- recursively evaluate an expression, the entry point
   re :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
-  re n m _  | length m > mx  =  error "toDynamicWithDefn: recursion limit reached"
-  re n m _  | n <= 0  =  error "toDynamicWithDefn: evaluation limit reached"
+  re n m _  | length m > mx  =  err "recursion limit reached"
+  re n m _  | n <= 0  =  err "evaluation limit reached"
   re n m (Value "if" _ :$ ec :$ ex :$ ey)  =  case rev n m ec of
     Nothing    -> Nothing
     Just (n,m,True)  -> re n m ex
@@ -151,7 +151,7 @@
     Just (n,m,True)  -> re n m eq
     Just (n,m,False) -> (n,m,) <$> toDynamic (val False)
   re n m e  =  case unfoldApp e of
-    [] -> error "toDynamicWithDefn: empty application unfold"  -- should never happen
+    [] -> err "empty application unfold"  -- should never happen
     [e] -> (n-1,m,) <$> toDynamic e
     (ef:exs) | ef == ef' -> red n m (foldApp (ef:map exprExpr exs))
              | otherwise -> foldl ($$) (re n m ef) exs
@@ -168,12 +168,14 @@
   -- should only be used to evaluate an expr of the form:
   -- ef' :$ exprExpr ex :$ exprExpr ey :$ ...
   red :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
-  red n m e  |  size e > n  =  error "toDynamicWithDefn: argument-size limit reached"
+  red n m e  |  size e > n  =  err "argument-size limit reached"
+  -- prevent recursion into negatives:
+  -- red n m e  |  any isNegative (unfoldApp e)  =  err "recursion into negatives"
   red n m e  =  case lookup e m of
-    Just Nothing -> error $ "toDynamicWithDefn: loop detected " ++ show e
+    Just Nothing -> err $ "loop detected " ++ show e
     Just (Just d) -> Just (n,m,d)
     Nothing -> case [re n ((e,Nothing):m) $ e' //- bs | (a',e') <- cx, Just bs <- [e `match` a']] of
-               [] -> error $ "toDynamicWithDefn: unhandled pattern " ++ show e
+               [] -> err $ "unhandled pattern " ++ show e
                (Nothing:_) -> Nothing
                (Just (n,m,d):_) -> Just (n,[(e',if e == e' then Just d else md) | (e',md) <- m],d)
 
@@ -183,6 +185,9 @@
                           Just (n', m', d2) -> (n',m',) <$> dynApply d1 d2
   _ $$ _               =  Nothing
 
+  err msg  =  -- trace (m ++ " for:\n" ++ showDefn cx)
+    error m  where  m = "Conjure.Defn.toDynamicWithDefn: " ++ msg
+
 -- | Evaluates an 'Expr' expression into 'Just' a regular Haskell value
 --   using a 'Defn' definition when it is found.
 --   If there's a type-mismatch, this function returns 'Nothing'.
@@ -215,7 +220,7 @@
 -- TODO: remove this from the interface?
 devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
 devalFast _ n [defn] x  =  reval defn n x
-devalFast _ _ _ _  =  error "devalFast: only works for singleton definitions"
+devalFast _ _ _ _  =  error "Conjure.Defn.devalFast: only works for singleton definitions"
 
 -- | Evaluates an 'Expr' expression into a regular Haskell value
 --   using a 'Defn' definition when it is found in the given expression.
@@ -226,7 +231,7 @@
 --
 -- (cf. 'toDynamicWithDefn', 'devaluate', deval')
 devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a
-devl ee n fxpr  =  deval ee n fxpr (error "devl: incorrect type?")
+devl ee n fxpr  =  deval ee n fxpr (error "Conjure.Defn.devl: incorrect type?")
 
 -- | Returns whether the given definition 'apparentlyTerminates'.
 defnApparentlyTerminates :: Defn -> Bool
diff --git a/src/Conjure/Defn/Redundancy.hs b/src/Conjure/Defn/Redundancy.hs
--- a/src/Conjure/Defn/Redundancy.hs
+++ b/src/Conjure/Defn/Redundancy.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Defn.Redundancy
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
diff --git a/src/Conjure/Defn/Test.hs b/src/Conjure/Defn/Test.hs
--- a/src/Conjure/Defn/Test.hs
+++ b/src/Conjure/Defn/Test.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Defn.Test
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
--- a/src/Conjure/Engine.hs
+++ b/src/Conjure/Engine.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Engine
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -19,6 +19,7 @@
   , conjureFromSpecWith
   , conjure0
   , conjure0With
+  , Results(..)
   , conjpure
   , conjpureWith
   , conjpureFromSpec
@@ -64,10 +65,10 @@
 --
 -- For example, given:
 --
--- > square :: Int -> Int
--- > square 0  =  0
--- > square 1  =  1
--- > square 2  =  4
+-- > factorial :: Int -> Int
+-- > factorial 2  =  2
+-- > factorial 3  =  6
+-- > factorial 4  =  24
 -- >
 -- > primitives :: [Prim]
 -- > primitives =
@@ -75,18 +76,20 @@
 -- >   , pr (1::Int)
 -- >   , prim "+" ((+) :: Int -> Int -> Int)
 -- >   , prim "*" ((*) :: Int -> Int -> Int)
+-- >   , prim "-" ((-) :: Int -> Int -> Int)
 -- >   ]
 --
 -- The conjure function does the following:
 --
--- > > conjure "square" square primitives
--- > square :: Int -> Int
--- > -- pruning with 14/25 rules
+-- > > conjure "factorial" factorial primitives
+-- > factorial :: Int -> Int
 -- > -- testing 3 combinations of argument values
--- > -- looking through 3 candidates of size 1
--- > -- looking through 3 candidates of size 2
--- > -- looking through 5 candidates of size 3
--- > square x  =  x * x
+-- > -- pruning with 27/65 rules
+-- > -- ...  ...  ...
+-- > -- looking through 185 candidates of size 7
+-- > -- tested 107 candidates
+-- > factorial 0  =  1
+-- > factorial x  =  x * factorial (x - 1)
 --
 -- The primitives list is defined with 'pr' and 'prim'.
 conjure :: Conjurable f => String -> f -> [Prim] -> IO ()
@@ -141,7 +144,37 @@
 -- | Like 'conjure' but allows setting the maximum size of considered expressions
 --   instead of the default value of 12.
 --
--- > conjureWithMaxSize 10 "function" function [...]
+-- > conjureWithMaxSize 18 "function" function [...]
+--
+-- For example, given the following partial definition for 'Data.List.insert':
+--
+-- > insert' :: Int -> [Int] -> [Int]
+-- > insert' 0 []  =  [0]
+-- > insert' 0 [1,2]  =  [0,1,2]
+-- > insert' 1 [0,2]  =  [0,1,2]
+-- > insert' 2 [0,1]  =  [0,1,2]
+--
+-- Conjure is able to find an appropriate definition at size 17
+-- with the following primitives:
+--
+-- > > conjureWithMaxSize 18 "insert" insert'
+-- > >   [ prim "[]" ([] :: [Int])
+-- > >   , prim ":" ((:) :: Int -> [Int] -> [Int])
+-- > >   , prim "<=" ((<=) :: Int -> Int -> Bool)
+-- > >   , prif (undefined :: [Int])
+-- > >   ]
+-- > insert :: Int -> [Int] -> [Int]
+-- > -- testing 4 combinations of argument values
+-- > -- pruning with 4/4 rules
+-- > -- ...  ...  ...
+-- > -- looking through 14550 candidates of size 17
+-- > -- tested 14943 candidates
+-- > insert x []  =  [x]
+-- > insert x (y:xs)  =  if x <= y
+-- >                     then x:insert y xs
+-- >                     else y:insert x xs
+--
+-- The default maximum size of 12 would not be enough for the above definition.
 conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()
 conjureWithMaxSize sz  =  conjureWith args
                        {  maxSize = sz
@@ -159,10 +192,13 @@
   , maxSearchTests        :: Int  -- ^ maximum number of tests to search for defined values
   , maxDeconstructionSize :: Int  -- ^ maximum size of deconstructions (e.g.: @_ - 1@)
 
-  -- advanced options --
+  -- advanced & debug options --
   , carryOn               :: Bool -- ^ whether to carry on after finding a suitable candidate
   , showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning
   , usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates
+  , showCandidates        :: Bool -- ^ (debug) show candidates -- warning: wall of text
+  , showTests             :: Bool -- ^ (debug) show tests
+  , showDeconstructions   :: Bool -- ^ (debug) show conjecture-and-allowed deconstructions
 
   -- pruning options --
   , rewriting             :: Bool -- ^ unique-modulo-rewriting candidates
@@ -170,6 +206,7 @@
   , adHocRedundancy       :: Bool -- ^ ad-hoc redundancy checks
   , copyBindings          :: Bool -- ^ copy partial definition bindings in candidates
   , atomicNumbers         :: Bool -- ^ restrict constant/ground numeric expressions to atoms
+  , requireZero           :: Bool -- ^ require 0 as base case for Num recursions
   , uniqueCandidates      :: Bool -- ^ unique-modulo-testing candidates
   }
 
@@ -184,6 +221,7 @@
 -- * search for defined applications for up to 100000 combinations
 -- * require recursive calls to deconstruct arguments
 -- * don't show the theory used in pruning
+-- * do not show tested candidates
 -- * do not make candidates unique module testing
 args :: Args
 args = Args
@@ -194,10 +232,13 @@
   , maxSearchTests         =  100000
   , maxDeconstructionSize  =   4
 
-  -- advanced options --
+  -- advanced & debug options --
   , carryOn                =  False
   , showTheory             =  False
   , usePatterns            =  True
+  , showCandidates         =  False
+  , showTests              =  False
+  , showDeconstructions    =  False
 
   -- pruning options --
   , rewriting              =  True
@@ -205,19 +246,20 @@
   , adHocRedundancy        =  True
   , copyBindings           =  True
   , atomicNumbers          =  True
+  , requireZero            =  True
   , uniqueCandidates       =  False
   }
 
 
 -- | Like 'conjure' but allows setting options through 'Args'/'args'.
 --
--- > conjureWith args{maxSize = 11} "function" function [...]
+-- > conjureWith args{maxSize = 18} "function" function [...]
 conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
 conjureWith args nm f  =  conjure0With args nm f (const True)
 
 -- | Like 'conjureFromSpec' but allows setting options through 'Args'/'args'.
 --
--- > conjureFromSpecWith args{maxSize = 11} "function" spec [...]
+-- > conjureFromSpecWith args{maxSize = 18} "function" spec [...]
 conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO ()
 conjureFromSpecWith args nm p  =  conjure0With args nm undefined p
 
@@ -225,8 +267,12 @@
 conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
 conjure0With args nm f p es  =  do
   print (var (head $ words nm) f)
-  when (length ts > 0) $
+  when (length ts > 0) $ do
     putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"
+    when (showTests args) $ do
+      putStrLn $ "{-"
+      putStr $ unlines $ map show ts
+      putStrLn $ "-}"
   putStrLn $ "-- pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"
   when (showTheory args) $ do
     putStrLn $ "{-"
@@ -241,6 +287,10 @@
       putStrLn $ "invalid:"
       putStr   $ unlines $ map showEq $ invalid thy
       putStrLn $ "-}"
+  when (showDeconstructions args) $ do
+    putStrLn $ "{- List of allowed deconstructions:"
+    putStr   $ unlines $ map show $ deconstructions results
+    putStrLn $ "-}"
   pr 1 0 rs
   where
   showEq eq  =  showExpr (fst eq) ++ " == " ++ showExpr (snd eq)
@@ -250,7 +300,8 @@
   pr n t ((is,cs):rs)  =  do
     let nc  =  length cs
     putStrLn $ "-- looking through " ++ show nc ++ " candidates of size " ++ show n
-    -- when (n<=12) $ putStrLn $ unlines $ map showDefn cs
+    when (showCandidates args) $
+      putStr $ unlines $ ["{-"] ++ map showDefn cs ++ ["-}"]
     case is of
       []     ->  pr (n+1) (t+nc) rs
       (_:_)  ->  do pr1 t is cs
@@ -263,36 +314,48 @@
     putStrLn $ showDefn i
     when (carryOn args) $ pr1 t' is (drop 1 cs'')
   rs  =  zip iss css
-  (iss, css, ts, thy)  =  conjpure0With args nm f p es
+  results  =  conjpure0With args nm f p es
+  iss  =  implementationss results
+  css  =  candidatess results
+  ts   =  bindings results
+  thy  =  theory results
   nRules  =  length (rules thy)
   nREs  =  length (equations thy) + nRules
 
 
+-- | Results to the 'conjpure' family of functions.
+-- This is for advanced users.
+-- One is probably better-off using the 'conjure' family.
+data Results = Results
+  { implementationss :: [[Defn]] -- ^ tiers of implementations
+  , candidatess :: [[Defn]]      -- ^ tiers of candidates
+  , bindings :: [Expr]           -- ^ test bindings used to verify candidates
+  , theory :: Thy                -- ^ the underlying theory
+  , deconstructions :: [Expr]    -- ^ the list of allowed deconstructions
+  }
+
+
 -- | Like 'conjure' but in the pure world.
 --
--- Returns a quadruple with:
---
--- 1. tiers of implementations
--- 2. tiers of candidates
--- 3. a list of tests
--- 4. the underlying theory
-conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+-- The most important part of the result are the tiers of implementations
+-- however results also include candidates, tests and the underlying theory.
+conjpure :: Conjurable f => String -> f -> [Prim] -> Results
 conjpure =  conjpureWith args
 
 -- | Like 'conjureFromSpec' but in the pure world.  (cf. 'conjpure')
-conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> Results
 conjpureFromSpec  =  conjpureFromSpecWith args
 
 -- | Like 'conjure0' but in the pure world.  (cf. 'conjpure')
-conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> Results
 conjpure0 =  conjpure0With args
 
 -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
-conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> Results
 conjpureWith args nm f  =  conjpure0With args nm f (const True)
 
 -- | Like 'conjureFromSpecWith' but in the pure world.  (cf. 'conjpure')
-conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
+conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> Results
 conjpureFromSpecWith args nm p  =  conjpure0With args nm undefined p
 
 -- | Like 'conjpure0' but allows setting options through 'Args' and 'args'.
@@ -301,8 +364,14 @@
 -- 'conjpure', 'conjpureWith', 'conjpureFromSpec', 'conjpureFromSpecWith',
 -- 'conjure', 'conjureWith', 'conjureFromSpec', 'conjureFromSpecWith' and
 -- 'conjure0' all refer to this.
-conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
-conjpure0With args@(Args{..}) nm f p es  =  (implementationsT, candidatesT, tests, thy)
+conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> Results
+conjpure0With args@(Args{..}) nm f p es  =  Results
+  { implementationss  =  implementationsT
+  , candidatess  =  candidatesT
+  , bindings  =  tests
+  , theory  =  thy
+  , deconstructions  =  deconstructions
+  }
   where
   tests  =  [ffxx //- bs | bs <- dbss]
   implementationsT  =  filterT implements candidatesT
@@ -311,7 +380,7 @@
                  && errorToFalse (p (cevl maxEvalRecursions fx))
   candidatesT  =  (if uniqueCandidates then nubCandidates args nm f else id)
                $  take maxSize candidatesTT
-  (candidatesTT, thy)  =  candidateDefns args nm f es
+  (candidatesTT, thy, deconstructions)  =  candidateDefns args nm f es
   ffxx   =  conjureApplication nm f
   vffxx  =  conjureVarApplication nm f
 
@@ -341,11 +410,17 @@
                             ++ (show . length $ equations thy) ++ " equations"
   printThy thy
   where
-  (_, _, _, thy)  =  conjpureWith args nm f es
+  Results {theory = thy}  =  conjpureWith args nm f es
 
 
 -- | Return apparently unique candidate definitions.
-candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
+--
+-- This function returns a trio:
+--
+-- 1. tiers of candidate definitions
+-- 2. an equational theory
+-- 3. a list of allowed deconstructions
+candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])
 candidateDefns args  =  candidateDefns' args
   where
   candidateDefns'  =  if usePatterns args
@@ -355,16 +430,17 @@
 
 -- | Return apparently unique candidate definitions
 --   where there is a single body.
-candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
-candidateDefns1 args nm f ps  =  first (mapT toDefn) $ candidateExprs args nm f ps
+candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])
+candidateDefns1 args nm f ps  =  first3 (mapT toDefn) $ candidateExprs args nm f ps
   where
   efxs  =  conjureVarApplication nm f
   toDefn e  =  [(efxs, e)]
+  first3 f (x,y,z)  =  (f x, y, z)
 
 
 -- | Return apparently unique candidate bodies.
-candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
-candidateExprs Args{..} nm f ps  =  (as \/ concatMapT (`enumerateFillings` recs) ts, thy)
+candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy, [Expr])
+candidateExprs Args{..} nm f ps  =  (as \/ concatMapT (`enumerateFillings` recs) ts, thy, deconstructions)
   where
   es  =  map fst ps
   ts | typ efxs == boolTy  =  foldAppProducts andE [cs, rs]
@@ -393,13 +469,15 @@
                     ,  m <- maybeToList (e `match` d)
                     ,  filter (uncurry (/=)) m == [(holeAsTypeOf e', e')]
                     ]
-    deconstructions :: [Expr]
-    deconstructions  =  filter (conjureIsDeconstruction f maxTests)
-                     $  concatMap candidateDeconstructionsFrom
-                     $  concat . take maxDeconstructionSize
-                     $  concatMapT forN [hs]
-      where
-      hs  =  nub $ conjureArgumentHoles f
+
+  deconstructions :: [Expr]
+  deconstructions  =  filter (conjureIsDeconstruction f maxTests)
+                   $  concatMap candidateDeconstructionsFrom
+                   $  concat . take maxDeconstructionSize
+                   $  concatMapT forN [hs]
+    where
+    hs  =  nub $ conjureArgumentHoles f
+
   recs  =  filterT keepR
         $  foldAppProducts ef [forN h | h <- conjureArgumentHoles f]
   thy  =  doubleCheck (===)
@@ -410,8 +488,8 @@
 
 -- | Return apparently unique candidate definitions
 --   using pattern matching.
-candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
-candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundant $ concatMapT fillingsFor fss,thy)
+candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])
+candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundant $ concatMapT fillingsFor fss,thy,deconstructions)
   where
   pats  =  conjurePats es nm f
   fss  =  concatMapT ps2fss pats
@@ -427,8 +505,8 @@
   appsWith :: Expr -> [Expr] -> [[Expr]]
   appsWith eh vs  =  enumerateAppsFor eh k $ vs ++ es
     where
-    k | atomicNumbers && conjureIsNumeric f eh  =  \e -> keepNumeric e && keep e
-      | otherwise                               =  keep
+    k | atomicNumbers && isNumeric eh  =  \e -> keepNumeric e && keep e
+      | otherwise                      =  keep
     -- discards non-atomic numeric ground expressions such as 1 + 1
     keepNumeric e  =  isFun e || isConst e || not (isGround e)
 
@@ -438,6 +516,8 @@
   hasRedundant | adHocRedundancy  =  hasRedundantRecursion
                | otherwise        =  const False
 
+  isNumeric  =  conjureIsNumeric f
+
   ps2fss :: [Expr] -> [[Defn]]
   ps2fss pats  =  discardT isRedundant
                .  products
@@ -453,7 +533,11 @@
                 .  tail
                 $  vars pat ++ [eh | any (uncurry should) (zip aess aes)]
       where
+      -- computes whether we should include a recurse for this given argument
+      -- numeric arguments additionally require 0 to be present as a case
+      -- for recursion
       should aes ae  =  length (nub aes) > 1 && hasVar ae && (isApp ae || isUnbreakable ae)
+                     && (not requireZero || not (isNumeric ae) || any isZero aes)
       aes   =                  (tail . unfoldApp . rehole) pat
       aess  =  transpose $ map (tail . unfoldApp . rehole) pats
 
@@ -480,13 +564,15 @@
                     ]
       where
       h = holeAsTypeOf e'
-    deconstructions :: [Expr]
-    deconstructions  =  filter (conjureIsDeconstruction f maxTests)
-                     $  concatMap candidateDeconstructionsFromHoled
-                     $  concat . take maxDeconstructionSize
-                     $  concatMapT (`appsWith` hs) [hs]
-      where
-      hs  =  nub $ conjureArgumentHoles f
+
+  deconstructions :: [Expr]
+  deconstructions  =  filter (conjureIsDeconstruction f maxTests)
+                   $  concatMap candidateDeconstructionsFromHoled
+                   $  concat . take maxDeconstructionSize
+                   $  concatMapT (`appsWith` hs) [hs]
+    where
+    hs  =  nub $ conjureArgumentHoles f
+
   recs ep  =  filterT (keepR ep)
            .  discardT (\e -> e == ep)
            $  recsV' (tail (vars ep))
diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs
--- a/src/Conjure/Expr.hs
+++ b/src/Conjure/Expr.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Expr
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -31,6 +31,7 @@
   , deholings
   , varToConst
   , hasAppInstanceOf
+  , isZero
   , isNegative
   , isStrictSubexprOf
 
@@ -537,6 +538,13 @@
   | all isApp es             =  listConflicts [ef | ef :$ _ <- es]
                             +++ listConflicts [ex | _ :$ ex <- es]
   | otherwise                =  [es | not (allEqual es)]
+
+-- | Is the epression encoding the number 0?
+--
+-- This function is sort of a hack.
+isZero :: Expr -> Bool
+isZero (Value "0" _)  =  True
+isZero _  =  False
 
 -- | Is the expression encoding a negative number.
 --
diff --git a/src/Conjure/Prim.hs b/src/Conjure/Prim.hs
--- a/src/Conjure/Prim.hs
+++ b/src/Conjure/Prim.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Prim
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -28,13 +28,24 @@
 import Test.LeanCheck.Utils
 
 
--- | A primtive expression (paired with instance reification).
+-- | A primitive expression (paired with instance reification).
+--   Create 'Prim's with 'pr' and 'prim'.
 type Prim  =  (Expr, Reification)
 
 
 -- | Provides a primitive value to Conjure.
 --   To be used on 'Show' instances.
 --   (cf. 'prim')
+--
+-- > conjure "fun" fun [ pr False
+-- >                   , pr True
+-- >                   , pr (0 :: Int)
+-- >                   , pr (1 :: Int)
+-- >                   , ...
+-- >                   ]
+--
+-- Argument types have to be monomorphized,
+-- so use type bindings when applicable.
 pr :: (Conjurable a, Show a) => a -> Prim
 pr x  =  (val x, conjureType x)
 
@@ -43,16 +54,71 @@
 --   To be used on values that are not 'Show' instances
 --   such as functions.
 --   (cf. 'pr')
+--
+-- > conjure "fun" fun [ ...
+-- >                   , prim "&&" (&&)
+-- >                   , prim "||" (||)
+-- >                   , prim "+" ((+) :: Int -> Int -> Int)
+-- >                   , prim "*" ((*) :: Int -> Int -> Int)
+-- >                   , prim "-" ((-) :: Int -> Int -> Int)
+-- >                   , ...
+-- >                   ]
+--
+-- Argument types have to be monomorphized,
+-- so use type bindings when applicable.
 prim :: Conjurable a => String -> a -> Prim
 prim s x  =  (value s x, conjureType x)
 
 
 -- | Provides an if condition bound to the given return type.
+--
+-- This should be used when one wants Conjure to consider
+-- if-expressions at all:
+--
+-- > last' :: [Int] -> Int
+-- > last' [x]  =  x
+-- > last' [x,y]  =  y
+-- > last' [x,y,z]  =  z
+--
+-- > > conjure "last" last' [ pr ([] :: [Int])
+-- > >                      , prim ":" ((:) :: Int -> [Int] -> [Int])
+-- > >                      , prim "null" (null :: [Int] -> Bool)
+-- > >                      , prif (undefined :: Int)
+-- > >                      , prim "undefined" (undefined :: Int)
+-- > >                      ]
+-- > last :: [Int] -> Int
+-- > -- ...  ...  ...
+-- > -- looking through 4 candidates of size 7
+-- > -- tested 5 candidates
+-- > last []  =  undefined
+-- > last (x:xs)  =  if null xs
+-- >                 then x
+-- >                 else last xs
 prif :: Conjurable a => a -> Prim
 prif x  =  (ifFor x, conjureType x)
 
 
 -- | Provides a case condition bound to the given return type.
+--
+-- This should be used when one wants Conjure to consider ord-case expressions:
+--
+-- > > conjure "mem" mem
+-- > >   [ pr False
+-- > >   , pr True
+-- > >   , prim "`compare`" (compare :: Int -> Int -> Ordering)
+-- > >   , primOrdCaseFor (undefined :: Bool)
+-- > >   ]
+-- > mem :: Int -> Tree -> Bool
+-- > -- ...  ...  ...
+-- > -- looking through 384 candidates of size 12
+-- > -- tested 371 candidates
+-- > mem x Leaf  =  False
+-- > mem x (Node t1 y t2)  =  case x `compare` y of
+-- >                          LT -> mem x t1
+-- >                          EQ -> True
+-- >                          GT -> mem x t2
+
+
 primOrdCaseFor :: Conjurable a => a -> Prim
 primOrdCaseFor x  =  (caseForOrd x, conjureType x)
 
diff --git a/src/Conjure/Reason.hs b/src/Conjure/Reason.hs
--- a/src/Conjure/Reason.hs
+++ b/src/Conjure/Reason.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Reason
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
diff --git a/src/Conjure/Red.hs b/src/Conjure/Red.hs
--- a/src/Conjure/Red.hs
+++ b/src/Conjure/Red.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Red
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
@@ -19,20 +19,75 @@
 import Conjure.Conjurable
 import Test.LeanCheck.Error (errorToFalse, errorToTrue)
 
--- | Checks if an expression is a deconstruction.
+-- | Returns whether an expression is a deconstruction
+--   based on the results of testing.
 --
--- There should be a single 'hole' in the expression.
+-- This function takes three arguments:
 --
--- It should decrease the size of all arguments that have
--- a size greater than 0.
+-- 1. a (conjurable) function from where type info is obtained
+-- 2. the maximum number of tests
+-- 3. an 'Expr' of a possible deconstruction.
+--
+-- To facilitate use, this function is often used in curried form
+-- in the contest of a "conjuring" function.  Given that the type
+-- of the function-to-be-conjured is '[Int] -> Int' and we would
+-- like to test for a maximum of 60 arguments, we would declare:
+--
+-- > > isDeconstruction = conjureIsDeconstruction (undefined :: [Int] -> Int) 60
+--
+-- Deconstructions are expressions that
+-- decrease the size of all arguments
+-- that have a size greater than 0.
+-- Here are some examples:
+--
+-- > > import Data.Express.Fixtures
+-- > > isDeconstruction  (minus :$ i_ :$ one)
+-- > True
+--
+-- > > isDeconstruction (tail' is_)
+-- > True
+--
+-- > > isDeconstruction (minus :$ i_ :$ two)
+-- > True
+--
+-- > decandidates = [minus :$ i_ :$ one, tail' is_, head' is_, zero -*- i_]
+-- > > filter isDeconstruction decandidates
+-- > [ _ - 1 :: Int
+-- > , tail _ :: [Int]
+-- > ]
+--
+-- Well formed deconstructions should have exactly one typed hole:
+--
+-- > > isDeconstruction (i_ -+- i_)
+-- > False
+--
+-- > > isDeconstruction (xx -+- one)
+-- > False
+--
+-- We can only deconstruct to the same type.
+-- Even though 'tail' is a deconstruction,
+-- 'head' is not.
+--
+-- > > isDeconstruction (head' is_)
+-- > False
+--
+-- Deconstructions should always reduce the size of expressions:
+--
+-- > > isDeconstruction (take' two is_)
+-- > False
+--
+-- Lastly we disallow deconstructions that always map to values of size 0.
+-- For the purposes of expression generation, in these cases
+-- we are better of not recursing at all and returning a constant value!
+--
+-- > > isDeconstruction (zero -*- i_)
+-- > False
 conjureIsDeconstruction :: Conjurable f => f -> Int -> Expr -> Bool
 conjureIsDeconstruction f maxTests ed
   =  length (holes ed) == 1  -- Well formed deconstruction, single hole.
   && typ h == typ ed         -- We can only deconstruct to the same type.
   && all is sizes            -- Do we always reduce size?
   && not (all iz sizes)      -- Disallow always mapping to values of size 0.
-                             -- In this case, we are better off not recursing
-                             -- and returning a constant value!
   where
   x << 0  =  True
   x << y  =  x < y
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
--- a/src/Conjure/Utils.hs
+++ b/src/Conjure/Utils.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Conjure.Utils
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,6 +1,6 @@
 # Stack file for the Conjure program generation library.
 #
-# Copyright (C) 2021-2024 Rudy Matela
+# Copyright (C) 2021-2025 Rudy Matela
 # Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 resolver: lts-21.25 # or ghc-9.4.8
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Test
--- Copyright   : (c) 2021-2024 Rudy Matela
+-- Copyright   : (c) 2021-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
diff --git a/test/Test/ListableExpr.hs b/test/Test/ListableExpr.hs
--- a/test/Test/ListableExpr.hs
+++ b/test/Test/ListableExpr.hs
@@ -1,6 +1,6 @@
 -- |
 -- Module      : Test.ListableExpr
--- Copyright   : (c) 2019-2024 Rudy Matela
+-- Copyright   : (c) 2019-2025 Rudy Matela
 -- License     : 3-Clause BSD  (see the file LICENSE)
 -- Maintainer  : Rudy Matela <rudy@matela.com.br>
 --
diff --git a/test/conjurable.hs b/test/conjurable.hs
--- a/test/conjurable.hs
+++ b/test/conjurable.hs
@@ -1,4 +1,4 @@
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 {-# Language DeriveDataTypeable, StandaloneDeriving #-}  -- for GHC < 7.10
diff --git a/test/defn.hs b/test/defn.hs
--- a/test/defn.hs
+++ b/test/defn.hs
@@ -1,4 +1,4 @@
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 import Test
@@ -46,7 +46,7 @@
   , errorToLeft (dvl factDefn (factV :$ val (10 :: Int)))
     == Right (3628800 :: Int)
   , errorToLeft (dvl factDefn (factV :$ val (11 :: Int)) == (39916800 :: Int))
-    == Left "toDynamicWithDefn: recursion limit reached"
+    == Left "Conjure.Defn.toDynamicWithDefn: recursion limit reached"
 
   , dvl fact1Defn (factV :$ val (0 :: Int)) == (1 :: Int)
   , dvl fact1Defn (factV :$ val (1 :: Int)) == (1 :: Int)
@@ -57,7 +57,7 @@
   , errorToLeft (dvl fact1Defn (factV :$ val (10 :: Int)))
     == Right (3628800 :: Int)
   , errorToLeft (dvl fact1Defn (factV :$ val (11 :: Int)) == (39916800 :: Int))
-    == Left "toDynamicWithDefn: recursion limit reached"
+    == Left "Conjure.Defn.toDynamicWithDefn: recursion limit reached"
 
   , dvl isZeroDefn (isZeroV :$ val (0 :: Int)) == True
   , dvl isZeroDefn (isZeroV :$ val (1 :: Int)) == False
diff --git a/test/derive.hs b/test/derive.hs
--- a/test/derive.hs
+++ b/test/derive.hs
@@ -1,4 +1,4 @@
--- Copyright (c) 2019-2024 Rudy Matela.
+-- Copyright (c) 2019-2025 Rudy Matela.
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE DeriveDataTypeable #-}
diff --git a/test/expr.hs b/test/expr.hs
--- a/test/expr.hs
+++ b/test/expr.hs
@@ -1,4 +1,4 @@
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 import Test
diff --git a/test/mk b/test/mk
--- a/test/mk
+++ b/test/mk
@@ -5,7 +5,7 @@
 # This tests that the makefile is thorough and actually
 # runs all tests scripts and benchmarks when asked to do so.
 #
-# Copyright (c) 2024 Rudy Matela.
+# Copyright (c) 2024-2025 Rudy Matela.
 # Distributed under the 3-Clause BSD licence.
 
 set -xe
diff --git a/test/red.hs b/test/red.hs
--- a/test/red.hs
+++ b/test/red.hs
@@ -1,4 +1,4 @@
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 import Test
diff --git a/test/sdist b/test/sdist
--- a/test/sdist
+++ b/test/sdist
@@ -2,7 +2,7 @@
 #
 # test/sdist: tests the package generated by "cabal sdist".
 #
-# Copyright (c) 2015-2024 Rudy Matela.
+# Copyright (c) 2015-2025 Rudy Matela.
 # Distributed under the 3-Clause BSD licence.
 
 set -xe
diff --git a/test/utils.hs b/test/utils.hs
--- a/test/utils.hs
+++ b/test/utils.hs
@@ -1,4 +1,4 @@
--- Copyright (C) 2021-2024 Rudy Matela
+-- Copyright (C) 2021-2025 Rudy Matela
 -- Distributed under the 3-Clause BSD licence (see the file LICENSE).
 
 import Test