diff --git a/limp.cabal b/limp.cabal
--- a/limp.cabal
+++ b/limp.cabal
@@ -1,5 +1,5 @@
 name:                limp
-version:             0.3.0.0
+version:             0.3.1.0
 synopsis:            representation of Integer Linear Programs
 description:         so far, this package just provides two representations for linear programs: "Numeric.Limp.Program", which is what I expect end-users to use, and
                      "Numeric.Limp.Canon", which is simpler, but would be less nice for writing linear programs.
@@ -9,7 +9,7 @@
 license-file:        LICENSE
 author:              Amos Robinson
 maintainer:          amos.robinson@gmail.com
-category:            numeric
+category:            Numeric
 build-type:          Simple
 cabal-version:       >=1.10
 homepage:            https://github.com/amosr/limp
@@ -36,7 +36,13 @@
         Numeric.Limp.Canon.Constraint
         Numeric.Limp.Canon.Convert
         Numeric.Limp.Canon.Program
+        Numeric.Limp.Canon.Pretty
         Numeric.Limp.Canon
+        Numeric.Limp.Canon.Analyse.Constants
+        Numeric.Limp.Canon.Simplify.Bounder
+        Numeric.Limp.Canon.Simplify.Crunch
+        Numeric.Limp.Canon.Simplify.Subst
+        Numeric.Limp.Canon.Simplify
 
   -- other-modules:       
   build-depends:
@@ -44,6 +50,23 @@
         containers  == 0.5.*
 
   ghc-options: -Wall -fno-warn-orphans
+  default-language: Haskell2010
+  default-extensions:       TemplateHaskell TypeFamilies FlexibleContexts GeneralizedNewtypeDeriving DataKinds GADTs RankNTypes StandaloneDeriving FlexibleInstances
+
+
+test-suite test
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs: tests
+  build-depends:
+        base        < 5,
+        containers  == 0.5.*,
+        tasty       == 0.10.*,
+        tasty-th    == 0.1.*,
+        tasty-quickcheck == 0.8.*,
+        QuickCheck       == 2.7.*,
+        limp
+
   default-language: Haskell2010
   default-extensions:       TemplateHaskell TypeFamilies FlexibleContexts GeneralizedNewtypeDeriving DataKinds GADTs RankNTypes StandaloneDeriving FlexibleInstances
 
diff --git a/src/Numeric/Limp/Canon/Analyse/Constants.hs b/src/Numeric/Limp/Canon/Analyse/Constants.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Limp/Canon/Analyse/Constants.hs
@@ -0,0 +1,41 @@
+-- | Analyse a program to find all constants
+module Numeric.Limp.Canon.Analyse.Constants where
+import Numeric.Limp.Canon.Program
+import Numeric.Limp.Rep
+
+import qualified Data.Map as M
+
+
+-- | Find the constants in a program, only by looking at the bounds with lo==up.
+-- (See "Numeric.Limp.Canon.Simplify.Stride" to convert constraints to bounds)
+constantsProgram :: (Ord z, Ord r, Rep c) => Program z r c -> Assignment z r c
+constantsProgram p
+ = mkAss $ concatMap eq $ M.toList $ _bounds p
+ where
+
+  eq (var, (Just lo, Just up))
+   | lo == up
+   = [(var, lo)]
+
+  eq _
+   = []
+
+  mkAss ms
+   = Assignment
+      (M.fromList $ concatMap tkLeft ms)
+      (M.fromList $ concatMap tkRight ms)
+
+  tkLeft (Left z, v)
+   -- Wow! What if the bounds aren't integral?
+   -- Well, I guess the ILP solver will eventually figure out it's infeasible.
+   -- Maybe it would be nice to trigger that error here.
+   | v == (fromZ $ truncate v)
+   = [(z, truncate v)]
+  tkLeft _
+   = []
+
+  tkRight (Right r, v)
+   = [(r, v)]
+  tkRight _
+   = []
+
diff --git a/src/Numeric/Limp/Canon/Constraint.hs b/src/Numeric/Limp/Canon/Constraint.hs
--- a/src/Numeric/Limp/Canon/Constraint.hs
+++ b/src/Numeric/Limp/Canon/Constraint.hs
@@ -16,6 +16,7 @@
  -- In order to be meaningful, at least one of lower or upper bound should be @Just@.
  = C1 (Maybe (R c)) (Linear z r c) (Maybe (R c))
 
+
 -- | Check whether an assignment satisfies the constraint
 check :: (Rep c, Ord z, Ord r) => Assignment z r c -> Constraint z r c -> Bool
 check a (Constraint cs) = all go cs
diff --git a/src/Numeric/Limp/Canon/Convert.hs b/src/Numeric/Limp/Canon/Convert.hs
--- a/src/Numeric/Limp/Canon/Convert.hs
+++ b/src/Numeric/Limp/Canon/Convert.hs
@@ -110,28 +110,14 @@
    = constraint $ P._constraints p
 
   bnds
-   = M.fromListWith merge
+   = M.fromListWith mergeBounds
    $ map extract
    $ P._bounds p
 
-  merge (l1,u1) (l2,u2)
-   = ( mmaybe max l1 l2
-     , mmaybe min u1 u2 )
-
-  mmaybe f a b
-   = case (a,b) of
-     (Nothing, Nothing)
-      -> Nothing
-     (Nothing, Just b')
-      -> Just $ b'
-     (Just a', Nothing)
-      -> Just $ a'
-     (Just a', Just b')
-      -> Just $ f a' b'
-
   extract :: Rep c => P.Bounds z r c -> (Either z r, (Maybe (R c), Maybe (R c)))
   extract (P.BoundZ (l,k,u))
    = (Left k, (fromZ <$> l, fromZ <$> u))
   extract (P.BoundR (l,k,u))
    = (Right k, (l,u))
+
 
diff --git a/src/Numeric/Limp/Canon/Linear.hs b/src/Numeric/Limp/Canon/Linear.hs
--- a/src/Numeric/Limp/Canon/Linear.hs
+++ b/src/Numeric/Limp/Canon/Linear.hs
@@ -10,12 +10,15 @@
 data Linear z r c
  = Linear (M.Map (Either z r) (R c))
 
+deriving instance (Ord z, Ord r, Rep c) => Eq (Linear z r c)
+deriving instance (Ord z, Ord r, Rep c) => Ord (Linear z r c)
+
 -- | Create linear function from list of variables and coefficients
-mkLinear :: (Ord z, Ord r)
+mkLinear :: (Ord z, Ord r, Rep c)
          => [(Either z r, R c)]
          -> Linear z r c
 mkLinear zrs
- = Linear (M.fromList zrs)
+ = Linear (M.fromListWith (+) zrs)
 
 
 -- | Evaluate linear function with given assignment
diff --git a/src/Numeric/Limp/Canon/Pretty.hs b/src/Numeric/Limp/Canon/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Limp/Canon/Pretty.hs
@@ -0,0 +1,84 @@
+module Numeric.Limp.Canon.Pretty where
+import Numeric.Limp.Canon.Constraint
+import Numeric.Limp.Canon.Linear
+import Numeric.Limp.Canon.Program
+import Numeric.Limp.Rep
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Data.Either
+
+instance (Show (Z c), Show (R c), Rep c, Show z, Show r, Ord z, Ord r) => Show (Program z r c) where
+ show = ppr show show
+
+ppr :: (Show (Z c), Show (R c), Rep c, Show z, Show r, Ord z, Ord r) => (z -> String) -> (r -> String) -> Program z r c -> String
+ppr pZ pR p
+ = unlines
+ [ "Minimize"
+ , indent $ pprL $ _objective p
+ , "Subject to"
+ , pprCs $ _constraints p
+ , "Bounds"
+ , pprBs $ _bounds p
+ , "Generals"
+ , pprGs $ varsOfProgram p ]
+
+ where
+  indent = ("\t"++)
+
+  pprV v
+   = filter (/=' ') $ either pZ pR v
+
+  pprL (Linear m)
+   = pprLf
+   $ M.toList m
+
+  pprLf xs@((_,c): _)
+   | c < 0
+   = "-" ++ pprLfs xs
+  pprLf xs
+   = pprLfs xs
+
+  pprLfs []
+   = ""
+  pprLfs [x]
+   = pprL1 x
+  pprLfs (x : rs@((_,c):_) )
+   =  pprL1 x
+   ++ (if c >= 0 then " + " else " - ")
+   ++ pprLfs rs
+
+  pprL1 (v,c) = show (abs c) ++ " " ++ pprV v
+
+  pprCs (Constraint cs)
+   = unlines $ map indent $ concatMap pprC cs
+
+  pprC (C1 lo f up)
+   =  case lo of
+       Nothing  -> []
+       Just lo' -> [pprL f ++ " >= " ++ show lo']
+   ++ case up of
+       Nothing  -> []
+       Just up' -> [pprL f ++ " <= " ++ show up']
+
+  pprLo (Just l)
+   = show l ++ " <= "
+  pprLo Nothing
+   = ""
+
+  pprUp (Just l)
+   = " <= " ++ show l
+  pprUp Nothing
+   = ""
+
+  pprBs m
+   = unlines $ map (indent.pprB) $ M.toList m
+
+  pprB (v, (lo,up))
+   = pprLo lo ++ pprV v ++ pprUp up
+
+  pprGs fvs
+   = unlines $ map pprV
+   $ filter isLeft
+   $ S.toList fvs
+
diff --git a/src/Numeric/Limp/Canon/Program.hs b/src/Numeric/Limp/Canon/Program.hs
--- a/src/Numeric/Limp/Canon/Program.hs
+++ b/src/Numeric/Limp/Canon/Program.hs
@@ -28,3 +28,38 @@
  , varsOfConstraint $ _constraints p
  , M.keysSet        $ _bounds      p ]
 
+
+-- | Merge some lower and upper bounds
+mergeBounds :: Rep c => (Maybe (R c), Maybe (R c)) -> (Maybe (R c), Maybe (R c)) -> (Maybe (R c), Maybe (R c))
+mergeBounds (l1,u1) (l2,u2)
+ = ( mmaybe max l1 l2
+   , mmaybe min u1 u2 )
+ where
+  mmaybe f a b
+   = case (a,b) of
+    (Nothing, Nothing)
+     -> Nothing
+    (Nothing, Just b')
+     -> Just $ b'
+    (Just a', Nothing)
+     -> Just $ a'
+    (Just a', Just b')
+     -> Just $ f a' b'
+
+
+-- | Check whether an assignment satisfies the program's constraints and bounds
+checkProgram :: (Rep c, Ord z, Ord r) => Assignment z r c -> Program z r c -> Bool
+checkProgram a p
+ =  check a (_constraints p)
+ && checkBounds a (_bounds p)
+
+checkBounds :: (Rep c, Ord z, Ord r) => Assignment z r c -> Map (Either z r) (Maybe (R c), Maybe (R c)) -> Bool
+checkBounds ass bs
+ =  M.fold (&&) True (M.mapWithKey checkB bs)
+ where
+  checkB k (lo,up)
+   = let v = zrOf ass k
+     in maybe True (<=v) lo
+     && maybe True (v<=) up
+     
+
diff --git a/src/Numeric/Limp/Canon/Simplify.hs b/src/Numeric/Limp/Canon/Simplify.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Limp/Canon/Simplify.hs
@@ -0,0 +1,27 @@
+-- | Perform some simple optimisations on program
+module Numeric.Limp.Canon.Simplify where
+import Numeric.Limp.Canon.Program
+import Numeric.Limp.Rep
+
+import Numeric.Limp.Canon.Analyse.Constants
+
+import Numeric.Limp.Canon.Simplify.Bounder
+import Numeric.Limp.Canon.Simplify.Crunch
+import Numeric.Limp.Canon.Simplify.Subst
+
+import Data.Monoid
+
+simplify :: (Ord z, Ord r, Rep c) => Program z r c -> (Assignment z r c, Program z r c)
+simplify p
+ = simplify' mempty p
+
+simplify' :: (Ord z, Ord r, Rep c) => Assignment z r c -> Program z r c -> (Assignment z r c, Program z r c)
+simplify' sub1 p
+ = let p'   = crunchProgram    p
+       p''  = bounderProgram   p'
+       sub2 = constantsProgram p''
+   in  if   assSize sub2 == 0
+       then (sub1, p'')
+       else simplify' (sub1 <> sub2) (substProgram sub2 p'')
+
+
diff --git a/src/Numeric/Limp/Canon/Simplify/Bounder.hs b/src/Numeric/Limp/Canon/Simplify/Bounder.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Limp/Canon/Simplify/Bounder.hs
@@ -0,0 +1,67 @@
+-- | Convert linear constraints that only mention one variable to bounds
+module Numeric.Limp.Canon.Simplify.Bounder where
+import Numeric.Limp.Canon.Constraint
+import Numeric.Limp.Canon.Linear
+import Numeric.Limp.Canon.Program
+import Numeric.Limp.Rep
+
+import Data.Either
+import qualified Data.Map as M
+
+type Bound z r c = (Either z r, (Maybe (R c), Maybe (R c)))
+
+
+-- | Convert a single constraint into a bound, if possible.
+--
+-- > bounder $ Constraint (5 <= y <= 10)
+-- > == Bound (Just 5) y (Just 10)
+--
+-- > bounder $ Constraint (5 <= 2y <= 10)
+-- > == Bound (Just 2.5) y (Just 5)
+--
+bounderConstraint1 :: (Ord z, Ord r, Rep c) => Constraint1 z r c -> Maybe (Bound z r c)
+bounderConstraint1 (C1 low (Linear mf) upp)
+ | M.size mf == 1
+ , [(k,c)]   <- M.toList mf
+ , c /= 0
+ = let fixup = (/ c)
+       low'  = fmap fixup low
+       upp'  = fmap fixup upp
+       bounds
+        | c >= 0
+        = (low',upp')
+        | otherwise
+        = (upp',low')
+   in  Just (k, bounds)
+
+ | otherwise
+ = Nothing
+   
+
+bounderConstraint :: (Ord z, Ord r, Rep c) => Constraint z r c -> (Constraint z r c, [Bound z r c])
+bounderConstraint (Constraint cs)
+ = let (cs', bs) = partitionEithers $ map bounderC cs
+   in  (Constraint cs', bs)
+ where
+  bounderC c
+   = case bounderConstraint1 c of
+     Nothing -> Left c
+     Just b  -> Right b
+   
+
+-- 
+bounderProgram :: (Ord z, Ord r, Rep c) => Program z r c -> Program z r c
+bounderProgram p
+ = let (c',bs) = bounderConstraint $ _constraints p
+   in p
+    { _constraints = c'
+    , _bounds      = foldl merge (_bounds p) bs }
+
+ where
+  merge m (k,v)
+   = case M.lookup k m of
+     Just v'
+      -> M.insert k (mergeBounds v' v) m
+     Nothing
+      -> M.insert k                 v  m
+
diff --git a/src/Numeric/Limp/Canon/Simplify/Crunch.hs b/src/Numeric/Limp/Canon/Simplify/Crunch.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Limp/Canon/Simplify/Crunch.hs
@@ -0,0 +1,54 @@
+-- | Crunch together all constraints with same linear function
+module Numeric.Limp.Canon.Simplify.Crunch where
+import Numeric.Limp.Canon.Constraint
+import Numeric.Limp.Canon.Program
+import Numeric.Limp.Rep
+
+import Data.List
+import Data.Function
+import Data.Maybe
+
+-- | Crunch the constraints in some program
+crunchProgram :: (Ord z, Ord r, Rep c) => Program z r c -> Program z r c
+crunchProgram p
+ = p { _constraints = crunchConstraint $ _constraints p }
+
+-- | Crunch some constraints.
+-- Constraints with the same function, for example
+--
+-- >              2x + y    < 5
+-- > &&   0 <     2x + y
+-- > &&           2x + y    < 10
+--
+-- becomes
+--
+-- >      0 <     2x + y    < 5
+--
+-- This should satisfy:
+--
+-- > forall a c. check a c == check a (crunchConstraint c)
+-- > forall a.   length (checkConstraint c) <= length c
+--
+crunchConstraint :: (Ord z, Ord r, Rep c) => Constraint z r c -> Constraint z r c
+crunchConstraint (Constraint cs)
+ = Constraint
+ $ map crunchC
+ $ groupBy ((==) `on` getLin) cs
+ where
+  getLin (C1 _   lin _  ) = lin
+  getLow (C1 low _   _  ) = low
+  getUpp (C1 _   _   upp) = upp
+
+  crunchC grp@(c:_)
+   = let low = compareMaybes maximum $ map getLow grp
+         upp = compareMaybes minimum $ map getUpp grp
+     in  C1 low (getLin c) upp
+
+  crunchC []
+   = error "Impossible - groupBy should not produce empty lists"
+
+  compareMaybes f ms
+   = case catMaybes ms of
+      ms'@(_:_) -> Just $ f ms'
+      []        -> Nothing
+
diff --git a/src/Numeric/Limp/Canon/Simplify/Subst.hs b/src/Numeric/Limp/Canon/Simplify/Subst.hs
new file mode 100644
--- /dev/null
+++ b/src/Numeric/Limp/Canon/Simplify/Subst.hs
@@ -0,0 +1,110 @@
+-- | Substitute an assignment into functions, constraints and programs
+module Numeric.Limp.Canon.Simplify.Subst where
+import Numeric.Limp.Canon.Constraint
+import Numeric.Limp.Canon.Linear
+import Numeric.Limp.Canon.Program
+import Numeric.Limp.Rep
+
+import qualified Data.Map as M
+
+
+-- | Substitute assignment into linear function.
+-- However, 'Linear' isn't quite a linear function! That is, it doesn't have a constant summand.
+-- So we must return the constant summand we lose.
+--
+-- Satisfies:
+--
+-- > forall a b f.
+-- > let (f', c') = substLinear a f
+-- > in  eval (a <> b) f == eval b f' + c'
+--
+-- > subst (x := 5) in 2x + y
+-- > (y, 10)
+--
+substLinear :: (Ord z, Ord r, Rep c) => Assignment z r c -> Linear z r c -> (Linear z r c, R c)
+substLinear (Assignment mz mr) (Linear mf)
+ = ( Linear $ M.fromList $ concatMap update mf'
+   ,          sum        $ map       getC   mf' )
+ where
+  mf' = M.toList mf
+
+  get (v,co)
+   | Left  z <- v
+   , Just zv <- M.lookup z mz
+   = Just $ fromZ zv * co
+   | Right r <- v
+   , Just rv <- M.lookup r mr
+   = Just $       rv * co
+
+   | otherwise
+   = Nothing
+
+  update vc
+   | Just _ <- get vc
+   = []
+   | otherwise
+   = [vc]
+
+  getC vc
+   | Just n <- get vc
+   = n
+   | otherwise
+   = 0
+
+
+-- | Substitute assignment into a single linear constraint.
+-- See 'substConstraint'.
+--
+-- > 5 <= 2x + y <= 10
+-- > subst (y := 3)
+-- > 2 <= 2x     <= 7
+--
+substConstraint1 :: (Ord z, Ord r, Rep c) => Assignment z r c -> Constraint1 z r c -> Constraint1 z r c
+substConstraint1 ass (C1 low lin upp)
+ = let (lin', const') = substLinear ass lin
+       fixup bound    = bound - const'
+   in C1 (fmap fixup low) lin' (fmap fixup upp)
+
+
+-- | Substitute assignment into a set of linear constraints.
+-- Satisfies:
+--
+-- > forall a b f.
+-- > let c' = substConstraint a c
+-- > in  check (a <> b) c == check b c'
+--
+-- > subst (x := 5) in 15 <= 2x + y <= 20
+-- > 5 <= y <= 10
+--
+substConstraint :: (Ord z, Ord r, Rep c) => Assignment z r c -> Constraint z r c -> Constraint z r c
+substConstraint ass (Constraint cs)
+ = Constraint
+ $ map (substConstraint1 ass) cs
+
+
+-- | Substitute assignment into a program.
+-- What does this satisfy? Hm.
+substProgram :: (Ord z, Ord r, Rep c) => Assignment z r c -> Program z r c -> Program z r c
+substProgram ass@(Assignment mz mr) p
+ = p
+ { _objective   = fst $ substLinear     ass $ _objective   p
+ , _constraints =       substConstraint ass $ _constraints p
+ , _bounds      =       cullBounds          $ _bounds      p
+ }
+ where
+  cullBounds
+   = M.mapMaybeWithKey cullB
+
+  cullB k v
+
+   | Left  z <- k
+   , Just  _ <- M.lookup z mz
+   = Nothing
+   | Right r <- k
+   , Just  _ <- M.lookup r mr
+   = Nothing
+
+   | otherwise
+   = Just v
+
+
diff --git a/src/Numeric/Limp/Program/Bounds.hs b/src/Numeric/Limp/Program/Bounds.hs
--- a/src/Numeric/Limp/Program/Bounds.hs
+++ b/src/Numeric/Limp/Program/Bounds.hs
@@ -8,6 +8,8 @@
  = BoundZ (B (Z c) z)
  | BoundR (B (R c) r)
 
+deriving instance (Show z, Show r, Show (Z c), Show (R c)) => (Show (Bounds z r c))
+
 -- | Maybe a lower bound, the variable's name, and maybe an upper bound.
 type B rep v
  = (Maybe rep, v, Maybe rep)
diff --git a/src/Numeric/Limp/Program/Constraint.hs b/src/Numeric/Limp/Program/Constraint.hs
--- a/src/Numeric/Limp/Program/Constraint.hs
+++ b/src/Numeric/Limp/Program/Constraint.hs
@@ -1,6 +1,7 @@
 module Numeric.Limp.Program.Constraint where
 import Numeric.Limp.Program.Linear
 import Numeric.Limp.Program.ResultKind
+import Numeric.Limp.Rep
 
 import Data.Monoid
 
@@ -39,6 +40,8 @@
  (:&&)   :: Constraint z r c -> Constraint z r c -> Constraint z r c
  (:!)    :: String           -> Constraint z r c -> Constraint z r c
  CTrue   ::                                         Constraint z r c
+
+deriving instance (Show z, Show r, Show (Z c), Show (R c)) => (Show (Constraint z r c))
 
 infix  5 :==
 infix  5 :<=
diff --git a/src/Numeric/Limp/Program/Eval.hs b/src/Numeric/Limp/Program/Eval.hs
--- a/src/Numeric/Limp/Program/Eval.hs
+++ b/src/Numeric/Limp/Program/Eval.hs
@@ -1,8 +1,10 @@
 -- | Functions for evaluating linear functions and checking constraints.
 module Numeric.Limp.Program.Eval where
 import Numeric.Limp.Rep
+import Numeric.Limp.Program.Bounds
 import Numeric.Limp.Program.Constraint
 import Numeric.Limp.Program.Linear
+import Numeric.Limp.Program.Program
 import Numeric.Limp.Program.ResultKind
 
 -- | Evaluate a linear function with given assignment.
@@ -51,3 +53,24 @@
 
   go CTrue
    = True
+
+-- | Check whether an assignment satisfies the program's constraints and bounds
+checkProgram :: (Rep c, Ord z, Ord r) => Assignment z r c -> Program z r c -> Bool
+checkProgram a p
+ =  check a (_constraints p)
+ && checkBounds a (_bounds p)
+
+checkBounds :: (Rep c, Ord z, Ord r) => Assignment z r c -> [Bounds z r c] -> Bool
+checkBounds ass bs
+ = all checkB bs
+ where
+  checkB (BoundZ (lo,z',up))
+   = checkBo (zOf ass z') lo up
+  checkB (BoundR (lo,r',up))
+   = checkBo (rOf ass r') lo up
+
+  checkBo v lo up
+   =  maybe True (<=v) lo
+   && maybe True (v<=) up
+     
+
diff --git a/src/Numeric/Limp/Program/Program.hs b/src/Numeric/Limp/Program/Program.hs
--- a/src/Numeric/Limp/Program/Program.hs
+++ b/src/Numeric/Limp/Program/Program.hs
@@ -11,6 +11,7 @@
 data Direction
  = Minimise
  | Maximise
+   deriving Show
 
 -- | Whole program, parameterised by:
 --
@@ -30,6 +31,8 @@
    -- Not all variables need to be mentioned, and if variables are mentioned multiple times, the intersection is used.
    , _bounds        :: [Bounds z r c]
    }
+
+deriving instance (Show z, Show r, Show (Z c), Show (R c)) => (Show (Program z r c))
 
 program :: Rep c => Direction -> Linear z r c k -> Constraint z r c -> [Bounds z r c] -> Program z r c
 program dir obj constr bounds
diff --git a/src/Numeric/Limp/Program/ResultKind.hs b/src/Numeric/Limp/Program/ResultKind.hs
--- a/src/Numeric/Limp/Program/ResultKind.hs
+++ b/src/Numeric/Limp/Program/ResultKind.hs
@@ -21,6 +21,8 @@
  LZ :: [(z, Z c)]          -> (Z c) -> Linear z r c KZ
  LR :: [(Either z r, R c)] -> (R c) -> Linear z r c KR
 
+deriving instance (Show z, Show r, Show (Z c), Show (R c)) => (Show (Linear z r c k))
+
 
 -- | Find the result type of merging, or adding, two linear functions:
 -- adding two integers produces an integer, while adding a real on either side produces a real.
diff --git a/src/Numeric/Limp/Rep.hs b/src/Numeric/Limp/Rep.hs
--- a/src/Numeric/Limp/Rep.hs
+++ b/src/Numeric/Limp/Rep.hs
@@ -10,6 +10,8 @@
 import Data.Map (Map)
 import qualified Data.Map as M
 
+import Data.Monoid
+
 -- | The Representation class. Requires its members @Z c@ and @R c@ to be @Num@, @Ord@ and @Eq@.
 --
 -- For some reason, for type inference to work, the members must be @data@ instead of @type@.
@@ -36,7 +38,12 @@
 
 deriving instance (Show (Z c), Show (R c), Show z, Show r) => Show (Assignment z r c)
 
+instance (Ord z, Ord r) => Monoid (Assignment z r c) where
+ mempty = Assignment M.empty M.empty
+ mappend (Assignment z1 r1) (Assignment z2 r2)
+  = Assignment (M.union z1 z2) (M.union r1 r2)
 
+
 -- | Retrieve value of integer variable - or 0, if there is no value.
 zOf :: (Rep c, Ord z) => Assignment z r c -> z -> Z c
 zOf (Assignment zs _) z
@@ -51,6 +58,9 @@
 zrOf :: (Rep c, Ord z, Ord r) => Assignment z r c -> Either z r -> R c
 zrOf a = either (fromZ . zOf a) (rOf a)
 
+assSize :: Assignment z r c -> Int
+assSize (Assignment mz mr)
+ = M.size mz + M.size mr
 
 
 -- | A representation that uses native 64-bit ints and 64-bit doubles.
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,15 @@
+
+import Test.Tasty
+
+import qualified Convert
+import qualified Simplify
+
+main = defaultMain properties
+
+properties :: TestTree
+properties
+ = testGroup "Properties"
+ [ Convert.tests
+ , Simplify.tests
+ ]
+