diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs
--- a/Yices/Painless/Language.hs
+++ b/Yices/Painless/Language.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE PatternGuards        #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE PatternGuards          #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE OverlappingInstances   #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
 {-# LANGUAGE FunctionalDependencies #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -28,6 +27,15 @@
 -- Terms and types are embedded in Haskell, so all the usual type
 -- inference and checking works for Yices propositions.
 --
+-- /A simple example: integers/
+--
+-- > import Yices.Painless.Language
+-- >
+-- > main = print =<< solve p
+-- >
+-- > p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool
+-- > p x y z = (3 * x) + (6 * y) ==* 1
+--
 -- /A simple example: bitvectors/
 --
 -- > solve $ \b1 (b2 :: Exp BitVector) 
@@ -86,7 +94,6 @@
 import qualified Data.Map as M
 
 import Data.Bits
-import qualified Data.Vector.Storable as V
 
 import Control.Monad
 import Control.Applicative ((<$>))
@@ -105,9 +112,6 @@
 --
 -- /Future work/:
 --
--- * Separate 'BitVector's into their own type, so that we can reuse
--- their 'Num' instance, avoiding OverlappingInstances.
---
 -- * BitVectors are sized, yet we do not represent their size at all
 -- currently.  Size types would let us statically check e.g. bit vector
 -- concatenation.
@@ -118,13 +122,17 @@
 --
 -- * A 'Monoid' instance for bit vectors?
 --
+-- * A monoid for conjunction?
+--
 -- * Support other numeric types.
 --
 -- * Support function types in the core language.
 --
--- * Support more Yices types: tuples, records, recursive types.
+-- * Support more SMT types: functions, tuples, records, recursive types.
 --
-
+-- * Deriving Exp. A (derivable) class for lifting Haskell data types
+-- into their symbolic form.
+--
 
 ------------------------------------------------------------------------
 -- Language
@@ -225,38 +233,16 @@
 -}
 
 instance (IsScalar t) => Prelude.Eq (Exp t) where
-  -- FIXME: instance makes no sense with standard signatures
+  -- instance makes no sense with standard signatures
   (==)        = error "Prelude.Eq.== applied to EDSL types"
 
 instance (IsScalar t) => Prelude.Ord (Exp t) where
-  -- FIXME: instance makes no sense with standard signatures
+  -- instance makes no sense with standard signatures
   compare     = error "Prelude.Ord.compare applied to EDSL types"
 
 ------------------------------------------------------------------------
 -- Bit vector operations
 
--- /TODO/ Vector Bool isn't an instance of num, but abstract Exp BitVectors are!
---
--- We could have an instance of Num BitVector and overload the operators.
--- via the Num (Exp a) instance.
---
-
-instance Num (Exp BitVector) where
-    (+)         = mkBVAdd
-    (-)         = mkBVSub
-    (*)         = mkBVMul
-    negate      = mkBVNeg
-
-    fromInteger n = constant . BitVector $
-                        V.generate (8 * sizeOf (undefined :: Word)) (testBit w)
-        where
-            w :: Word
-            w = fromIntegral n
-
-    abs _       = error "Prelude.Num.abs applied to EDSL types"
-    -- if n >= 0 then n else negate n
-    signum _    = error "Prelude.Num.signum applied to EDSL types"
-
     -- TODO: fromInteger should probably build from mkBVConstant
     -- TOD0: need size information.
     -- TOD0: support construction of a specific size
@@ -267,17 +253,24 @@
    -- needs size types!
 
 -- $BitInstances
--- The 'Exp BitVector' type is an instance of 'Bits', allowing the usual
+-- The 'Exp BitVector' type is an instance of 'Bits' and 'Num', allowing the usual
 -- Haskell bitwise operators to be used to construct propositions involving
 -- bitwise operations on bit vectors.
 --
--- > (.&,), (.|.), xor, complement, shiftL, shiftR
+-- > (.&.) :: Exp BitVector -> Exp BitVector -> Exp BitVector
+-- > (.|.)
+-- > xor
+-- > complement
+-- > shiftL
+-- > shiftR
 --
 -- Currently bit vectors are fixed at 'sizeOf (undefined :: Word)' bits.
 --
 -- Bit vector constants can be constructed using overloaded numeric
 -- literals.
 --
+-- TODO: instance Bits a => Bits (Exp a)
+--
 
 instance Bits (Exp BitVector) where
     (.&.)       = mkBVAnd
@@ -288,7 +281,6 @@
     shiftR      = mkBVShiftR0
     isSigned _  = False
     bitSize  _  = 8 * sizeOf (undefined :: Word) -- TODO! size type
-        
 
 ------------------------------------------------------------------------
 
@@ -357,17 +349,10 @@
 
 -- Bit vector operators
 
-mkBVAdd :: Exp BitVector -> Exp BitVector -> Exp BitVector
-mkBVAdd x y = PrimBVAdd `PrimApp` tup2 (x, y)
-
-mkBVMul :: Exp BitVector -> Exp BitVector -> Exp BitVector
-mkBVMul x y = PrimBVMul `PrimApp` tup2 (x, y)
-
-mkBVSub :: Exp BitVector -> Exp BitVector -> Exp BitVector
-mkBVSub x y = PrimBVSub `PrimApp` tup2 (x, y)
+-- mkBVNeg :: Exp BitVector -> Exp BitVector
+-- mkBVNeg x = PrimBVNeg `PrimApp` x
 
-mkBVNeg :: Exp BitVector -> Exp BitVector
-mkBVNeg x = PrimBVNeg `PrimApp` x
+-- Bits instance
 
 mkBVAnd :: Exp BitVector -> Exp BitVector -> Exp BitVector
 mkBVAnd x y = PrimBVAnd `PrimApp` tup2 (x, y)
@@ -387,8 +372,11 @@
 mkBVShiftR0 :: Exp BitVector -> Int -> Exp BitVector
 mkBVShiftR0 x n = PrimBVSR0 `PrimApp` tup2 (x, constant n) -- shiftR fills with 0
 
--- Operators from Num
+------------------------------------------------------------------------
+-- Scalar operations
 
+-- Operators from Num, also includes BitVector operations
+
 mkAdd :: (IsNum t) => Exp t -> Exp t -> Exp t
 mkAdd x y = PrimAdd numType `PrimApp` tup2 (x, y)
 
@@ -429,6 +417,7 @@
 mkLNot :: Exp Bool -> Exp Bool
 mkLNot x = PrimLNot `PrimApp` x
 
+------------------------------------------------------------------------
 -- Smart constructor for literals
 
 -- | Literal 'True'
@@ -990,7 +979,7 @@
     = do mn <- Yices.getValueBool m d
          return (v, YValue mn)
 
-    | NonNumScalarType (TypeVectorBool _)                <- ty
+    | NumScalarType (IntegralNumType (TypeVectorBool _))               <- ty
     = do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word))
          return (v, YValue $ fmap BitVector mn)
             
@@ -1048,7 +1037,7 @@
 
         -- Bit vectors
         go (OLam (f :: OpenFun (env, a) t)) n g
-            | ty@(NonNumScalarType (TypeVectorBool _))                <- scalarType :: ScalarType a
+            | ty@(NumScalarType (IntegralNumType (TypeVectorBool _)))   <- scalarType :: ScalarType a
             = do
                 let nm = "x" ++ show n
                 -- TODO: hack, no size information for bit vectors yet.
@@ -1083,7 +1072,7 @@
     = if n then Yices.mkTrue  c
            else Yices.mkFalse c
 
-    | NonNumScalarType (TypeVectorBool _)            <- scalarType :: ScalarType t
+    | NumScalarType (IntegralNumType (TypeVectorBool _))  <- scalarType :: ScalarType t
     = Yices.mkBVConstantFromVector c (unBV n)
 
 
@@ -1118,7 +1107,7 @@
             Yices.mkNeq c e1 e2
 
 -- Specialize for BitVector first
-exec c (OPrimApp  (PrimLt (NonNumScalarType (TypeVectorBool _)))
+exec c (OPrimApp  (PrimLt (NumScalarType (IntegralNumType (TypeVectorBool _))))
         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
@@ -1132,7 +1121,7 @@
             Yices.mkLt c e1 e2
 
 -- Specialize for BitVector first
-exec c (OPrimApp  (PrimLtEq (NonNumScalarType (TypeVectorBool _)))
+exec c (OPrimApp  (PrimLtEq (NumScalarType (IntegralNumType (TypeVectorBool _))))
         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
@@ -1145,7 +1134,7 @@
             Yices.mkLe c e1 e2
 
 -- Specialize for BitVector first
-exec c (OPrimApp  (PrimGt (NonNumScalarType (TypeVectorBool _)))
+exec c (OPrimApp  (PrimGt (NumScalarType (IntegralNumType (TypeVectorBool _))))
         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
@@ -1159,7 +1148,7 @@
 
 -- TODO think about what gets through the overloading incorrectly.
 -- Specialize for BitVector first
-exec c (OPrimApp  (PrimGtEq (NonNumScalarType (TypeVectorBool _)))
+exec c (OPrimApp  (PrimGtEq (NumScalarType (IntegralNumType (TypeVectorBool _))))
         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
@@ -1189,45 +1178,49 @@
 
 -- Numerical operations
 
-exec c (OPrimApp  (PrimAdd _)
-        (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
+-- overloaded on bit vectors
+exec c (OPrimApp  (PrimAdd (IntegralNumType (TypeVectorBool _)))
+          (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
-            Yices.mkSum c [e1,e2]
+            Yices.mkBVAdd c e1 e2
 
-exec c (OPrimApp  (PrimSub _)
+exec c (OPrimApp  (PrimAdd _)
         (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
-            Yices.mkSub c [e1,e2]
+            Yices.mkSum c [e1,e2]
 
-exec c (OPrimApp  (PrimMul _)
+-- overloaded on bit vectors
+exec c (OPrimApp  (PrimSub (IntegralNumType (TypeVectorBool _)))
           (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
-            Yices.mkMul c [e1,e2]
-
-------------------------------------------------------------------------
--- Bit Vector operations
+            Yices.mkBVSub c e1 e2
 
-exec c (OPrimApp PrimBVAdd
-          (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
+exec c (OPrimApp  (PrimSub _)
+        (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
-            Yices.mkBVAdd c e1 e2
+            Yices.mkSub c [e1,e2]
 
-exec c (OPrimApp PrimBVMul
+-- overloaded on bit vectors
+exec c (OPrimApp  (PrimMul (IntegralNumType (TypeVectorBool _)))
           (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
             Yices.mkBVMul c e1 e2
 
-exec c (OPrimApp PrimBVSub
+exec c (OPrimApp  (PrimMul _)
           (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do
             e1 <- exec c x1
             e2 <- exec c x2
-            Yices.mkBVSub c e1 e2
+            Yices.mkMul c [e1,e2]
 
+------------------------------------------------------------------------
+-- Bit Vector operations
+
+-- TODO
 exec c (OPrimApp PrimBVNeg
           (OTuple (NilTup `SnocTup` x1))) = do
             e1 <- exec c x1
diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs
--- a/Yices/Painless/Type.hs
+++ b/Yices/Painless/Type.hs
@@ -136,6 +136,8 @@
   TypeCLLong  :: IntegralDict CLLong  -> IntegralType CLLong
   TypeCULLong :: IntegralDict CULLong -> IntegralType CULLong
 
+  TypeVectorBool  :: IntegralDict BitVector -> IntegralType BitVector
+
 -- |Floating-point types supported in yices computations.
 --
 data FloatingType a where
@@ -153,16 +155,35 @@
   TypeCSChar  :: NonNumDict CSChar    -> NonNumType CSChar
   TypeCUChar  :: NonNumDict CUChar    -> NonNumType CUChar
 
-  -- Could define a Num instance
-  TypeVectorBool  :: NonNumDict BitVector    -> NonNumType BitVector
-
-
 ------------------------------------------------------------------------
 
 -- Todo: support 'Word' packed representation (for fast constants).
 newtype BitVector = BitVector { unBV :: V.Vector Bool }
     deriving (Eq, Ord, Typeable)
 
+instance Num BitVector where
+    (+)         = error "Prelude.Num.+ applied to BitVectors"
+    (-)         = error "Prelude.Num.- applied to BitVectors"
+    (*)         = error "Prelude.Num.* applied to BitVectors"
+    negate      = error "Prelude.Num.negate applied to BitVectors"
+    abs _       = error "Prelude.Num.abs applied to EDSL types"
+    signum _    = error "Prelude.Num.signum applied to EDSL types"
+
+    -- TODO: size is fixed
+    fromInteger n = BitVector $ V.generate (8 * sizeOf (undefined :: Word)) (testBit w)
+        where
+            w :: Word
+            w = fromIntegral n
+
+-- Fake instances so we can get Num BitVector. We could do it for real via Integer...
+-- Or just use Integers
+
+instance Integral BitVector
+instance Bits     BitVector
+instance Enum     BitVector
+instance Bounded  BitVector
+instance Real     BitVector
+
 -- Smart show instance.
 instance Show BitVector where
     show (BitVector v) 
@@ -215,6 +236,7 @@
   show (TypeCULong _)  = "CULong"
   show (TypeCLLong _)  = "CLLong"
   show (TypeCULLong _) = "CULLong"
+  show (TypeVectorBool _) = "(Vector Bool)"
 
 instance Show (FloatingType a) where
   show (TypeFloat _)   = "Float"
@@ -228,7 +250,6 @@
   show (TypeCChar _)  = "CChar"
   show (TypeCSChar _) = "CSChar"
   show (TypeCUChar _) = "CUChar"
-  show (TypeVectorBool _) = "(Vector Bool)"
 
 instance Show (NumType a) where
   show (IntegralNumType ty) = show ty
@@ -253,6 +274,9 @@
 instance IsIntegral Int where
   integralType = TypeInt IntegralDict
 
+instance IsIntegral BitVector where
+  integralType = TypeVectorBool IntegralDict
+
 instance IsIntegral Int8 where
   integralType = TypeInt8 IntegralDict
 
@@ -341,9 +365,6 @@
 instance IsNonNum CUChar where
   nonNumType = TypeCUChar NonNumDict
 
-instance IsNonNum BitVector where
-  nonNumType = TypeVectorBool NonNumDict
-
 -- |Numeric types
 --
 class (Num a, IsScalar a) => IsNum a where
@@ -403,6 +424,9 @@
 instance IsNum CULLong where
   numType = IntegralNumType integralType
 
+instance IsNum BitVector where
+  numType = IntegralNumType integralType
+
 instance IsNum Float where
   numType = FloatingNumType floatingType
 
@@ -423,6 +447,9 @@
 instance IsBounded Int where
   boundedType = IntegralBoundedType integralType
 
+instance IsBounded BitVector where
+  boundedType = IntegralBoundedType integralType
+
 instance IsBounded Int8 where
   boundedType = IntegralBoundedType integralType
 
@@ -560,6 +587,9 @@
 instance IsScalar CDouble where
   scalarType = NumScalarType numType
 
+instance IsScalar BitVector where
+  scalarType = NumScalarType numType
+
 -- Non-numerical scalar types
 
 instance IsScalar Bool where
@@ -577,9 +607,6 @@
 instance IsScalar CUChar where
   scalarType = NonNumScalarType nonNumType
 
-instance IsScalar BitVector where
-  scalarType = NonNumScalarType nonNumType -- false for bitvectors...
-
 -- Extract reified dictionaries
 -- 
 
@@ -602,6 +629,7 @@
 integralDict (TypeCULong  dict) = dict
 integralDict (TypeCLLong  dict) = dict
 integralDict (TypeCULLong dict) = dict
+integralDict (TypeVectorBool dict) = dict
 
 floatingDict :: FloatingType a -> FloatingDict a
 floatingDict (TypeFloat dict) = dict
@@ -615,7 +643,6 @@
 nonNumDict (TypeCChar  dict) = dict
 nonNumDict (TypeCSChar dict) = dict
 nonNumDict (TypeCUChar dict) = dict
-nonNumDict (TypeVectorBool dict) = dict
 
 -- Tuple type
 -- ----------
diff --git a/tests/examples/ex1.hs b/tests/examples/ex1.hs
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex1.hs
@@ -0,0 +1,5 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p = 0 ==* (1 :: Exp Int)
diff --git a/tests/examples/ex2.hs b/tests/examples/ex2.hs
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex2.hs
@@ -0,0 +1,5 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p = false
diff --git a/tests/examples/ex24.hs b/tests/examples/ex24.hs
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex24.hs
@@ -0,0 +1,16 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+data S = S1 | S2 | S3
+    deriving (Show, Enum)
+
+p x1 x2 x3 x4 = 
+    and 
+      [ (/=*) x1 x2
+      , (/=*) x1 x3
+      , (/=*) x1 x4
+      , (/=*) x2 x3
+      , (/=*) x2 x4
+      , (/=*) x3 x4
+      ]
diff --git a/tests/examples/ex3.hs b/tests/examples/ex3.hs
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex3.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Yices.Painless.Language
+import Prelude hiding (and)
+
+main = print =<< solve p
+
+-- Currently, need to derive Int, then translate in and out.
+
+data PC = Sleeping | Trying | Critical
+    deriving (Show, Enum)
+
+p x1 x2 z1 z2 (w1 :: Exp Int) (w2 :: Exp Int) =
+  and
+    [ x1 ==* x2
+    , x1 ==* z1
+    , x2 ==* fromIntegral (fromEnum Critical)
+    , x2 ==* z2
+    , x2 ==* w1
+    , x1 ==* fromIntegral (fromEnum Trying)
+    ]
+
+{-
+-- (define-type pc (scalar sleeping trying critical))
+(define x1::pc)
+(define x2::pc)
+(define z1::pc)
+(define z2::pc)
+(define w1::pc)
+(define w2::pc)
+
+(assert (= x1 x2))
+(assert (= x1 z1))
+(assert (= x2 critical))
+(assert (= x2 z2))
+(assert (= z2 w1))
+(assert (= x1 trying))
+-}
diff --git a/tests/examples/ex5.ys b/tests/examples/ex5.ys
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex5.ys
@@ -0,0 +1,18 @@
+
+(define-type pc (scalar sleeping trying critical))
+(define f::(-> pc pc))
+(define g::(-> pc pc))
+(define x1::pc)
+(define x2::pc)
+(define x3::pc)
+(define x4::pc)
+(define x5::pc)
+(define x6::pc)
+
+
+
+(assert (/= (g (f x1)) (g (f x2))))
+(assert (= x1 x3))
+(assert (= x1 x4))
+(assert (= x3 x2))
+
diff --git a/tests/examples/ex6.ys b/tests/examples/ex6.ys
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex6.ys
@@ -0,0 +1,18 @@
+
+(define-type pc (scalar sleeping trying critical))
+(define f::(-> pc pc))
+(define g::(-> pc pc))
+(define x1::pc)
+(define x2::pc)
+(define x3::pc)
+(define x4::pc)
+(define x5::pc)
+(define x6::pc)
+
+
+
+(assert (= x1 x3))
+(assert (= x1 x4))
+(assert (= x3 x2))
+(assert (/= (g (f x1)) (g (f x2))))
+
diff --git a/tests/examples/ex66.hs b/tests/examples/ex66.hs
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex66.hs
@@ -0,0 +1,7 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool
+p x y z = (3 * x) + (6 * y) ==* 1
+
diff --git a/tests/examples/ex67.hs b/tests/examples/ex67.hs
new file mode 100644
--- /dev/null
+++ b/tests/examples/ex67.hs
@@ -0,0 +1,10 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool 
+p x y z =
+    (3 * x) + (6 * y) + z ==* 1
+  &&*
+    z ==* 2
+
diff --git a/yices-painless.cabal b/yices-painless.cabal
--- a/yices-painless.cabal
+++ b/yices-painless.cabal
@@ -1,5 +1,5 @@
 Name:                yices-painless
-Version:             0.1
+Version:             0.1.1
 Synopsis:            An embedded language for programming the Yices SMT solver
 Description:         
     This library defines an embedded language in Haskell for programming
@@ -26,9 +26,16 @@
     .
     * <http://yices.csl.sri.com/>
     .
-    Low and medium-level bindings to the Yices C API are also provided.
-    The medium-level bindings add significant type and resource safety
-    to that which the C API provides.
+    The primary interface is via the EDSL, "Yices.Painless.Language",
+    however, low and medium-level bindings to the Yices C API are also provided
+    ("Yices.Painless.Base.C" and "Yices.Painless.Base"). The
+    medium-level bindings add significant type and resource safety to
+    that which the C API provides.
+    .
+    Documentation for this package is available:
+    .
+    * <http://www.galois.com/~dons/yices-painless/>
+    .
 
 Homepage:            http://code.haskell.org/~dons/code/yices-painless
 License:             BSD3